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.

Featured content

Scaling the Everest of software security with Dr. Jonathan Protzenko

Episode 58, January 9, 2019 - Dr. Protzenko talks about what’s wrong with software (and why it’s vitally important to get it right), explains why there are so many programming languages (and tells us about a few he’s been working on), and finally, acts as our digital Sherpa for Project Everest, an assault on software integrity and confidentiality that aims to build and deploy a verified HTTPS stack.