Jonathan Protzenko
Principal Researcher
About
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)
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) (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.
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.