Portrait of Jonathan Protzenko

Jonathan Protzenko

Senior Researcher


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