Portrait of Jonathan Protzenko

Jonathan Protzenko

Principal Researcher

About

See my personal web page 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 from 2010 to 2014.

Learn more about my work in the press: Quanta Magazine, IEEE Explore!, CACM

Projects:

  • 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), a compiler from Low* to C, 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 that now has 200,000 users.