Portrait of Jonathan Protzenko

Jonathan Protzenko

Principal Researcher


See my personal web page (opens in new tab) for an up-to-date list of publications, and more information about my current projects.

I am a Principal Researcher in the RiSE group, which I joined in Fall 2014. Previously, I was at INRIA Paris (opens in new tab) from 2010 to 2014.

Learn more about my work in the press: Quanta Magazine (opens in new tab), IEEE Explore! (opens in new tab), CACM (opens in new tab)


  • Computational Law (Catala): bringing the rigor of formal methods to the legal world, specifically statutory law.
  • Verified Protocol Stacks (Noise*, Signal*, MLS*): low-level, efficient, verified implementations of popular cryptographic protocols.
  • Low-Level Programming in F* (a.k.a. Low*): I wrote KaRaMeL (née KReMLin) (opens in new tab), a compiler from Low* to C (opens in new tab), and co-lead several high-profile projects written in Low*, such as: HACL*, EverCrypt, EverQUIC, parts of which have been integrated into Windows, Linux, Firefox, Tezos, mbedTLS, and many more.

On my free time, I maintain several open-source projects, including a Thunderbird addon (opens in new tab) that now has 200,000 users.