Jonathan Protzenko

I am a Researcher in the RiSE group, which I joined in Fall 2014. Previously, I was at INRIA Paris from 2010 to 2014.

My research involves verifying critical code and bringing it into existing software ecosystems. To that end, I wrote KReMLin, a compiler from F* to C. Code compiled by KReMLin has been integrated into Windows, Firefox, the mbedTLS library, the Tezos blockchain, and soon the Linux kernel. In addition to tooling, I am deeply involved with the following software verification projects:

• HACL*, a collection of verified cryptographic algorithms, verified in F*, compiled to C
• EverCrypt, a complete cryptographic library that offers abstraction, multiplexing, agility and CPU auto-detection, verified in F*, compiled to C and assembly
• miTLS, a verified implementation of QUIC and TLS 1.2/1.3 in F*, compiled to C

All of these works are part of the Everest project, an ambitious research effort spanning three continents, five institutions and twelve time zones.

On my free time, I maintain several open-source projects, including a Thunderbird addon that now has 200,000 users.

More information as well as an up-to-date list of publications can be found on my personal web page.