Illustrating the Mezzo programming language. - Jonathan Protzenko (FSFMA, 2013)

Programming with permissions in Mezzo. - François Pottier; Jonathan Protzenko (ICFP, 2013)

The implementation of the Mezzo type-checker. - Jonathan Protzenko (IFL, 2013)

The ins and outs of iteration in Mezzo. - Armaël Guéneau; François Pottier; Jonathan Protzenko (CoRR, 2013)

Type Soundness and Race Freedom for Mezzo. - Thibaut Balabonski; François Pottier; Jonathan Protzenko (FLOPS, 2014)

Mezzo: a typed language for safe effectful concurrent programs. (Mezzo: un langage typé pour programmer de manière concurrent et sure en présence d'effets). - Jonathan Protzenko (2014)

Global Sequence Protocol: A Robust Abstraction for Replicated Shared State. - Sebastian Burckhardt; Daan Leijen; Jonathan Protzenko; Manuel Fähndrich (ECOOP, 2015)

Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment. - Thomas Ball 001; Sebastian Burckhardt; Jonathan de Halleux; Michal Moskal; Jonathan Protzenko; Nikolai Tillmann (MOBILESoft, 2015)

Functional Pearl: the Proof Search Monad. - Jonathan Protzenko (IWIL@LPAR, 2015)

Implementing real-time collaboration in TouchDevelop using AST merges. - Jonathan Protzenko; Sebastian Burckhardt; Michal Moskal; Jedidiah McClurg (MobileDeLi, 2015)

A Few Lessons from the Mezzo Project. - François Pottier; Jonathan Protzenko (SNAPL, 2015)

Microsoft touch develop and the BBC micro: bit. - Thomas Ball 001; Jonathan Protzenko; Judith Bishop; Michal Moskal; Jonathan de Halleux; Michael Braun; Steve Hodges 001; Clare Riley (ICSE (Companion Volume), 2016)

Dijkstra Monads for Free. - Danel Ahman; Catalin Hritcu; Guido Martínez; Gordon D. Plotkin; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy (CoRR, 2016)

Abstract Specifications for Weakly Consistent Data. - Sebastian Burckhardt; Jonathan Protzenko (IEEE Data Eng. Bull., 2016)

Implementing and Proving the TLS 1.3 Record Layer. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Markulf Kohlweiss; Jianyang Pan; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin; Jean Karim Zinzindohoue (IACR Cryptol. ePrint Arch., 2016)

The Design and Formalization of Mezzo, a Permission-Based Programming Language. - Thibaut Balabonski; François Pottier; Jonathan Protzenko (ACM Trans. Program. Lang. Syst., 2016)

Dijkstra monads for free. - Danel Ahman; Catalin Hritcu; Kenji Maillard; Guido Martínez; Gordon D. Plotkin; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy (POPL, 2017)

Everest: Towards a Verified, Drop-in Replacement of HTTPS. - Karthikeyan Bhargavan; Barry Bond; Antoine Delignat-Lavaud; Cédric Fournet; Chris Hawblitzel; Catalin Hritcu; Samin Ishtiaq; Markulf Kohlweiss; K. Rustan M. Leino; Jay R. Lorch; Kenji Maillard; Jianyang Pan; et al. (SNAPL, 2017)

Verified Low-Level Programming Embedded in F*. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (CoRR, 2017)

A Monadic Framework for Relational Verification (Functional Pearl). - Niklas Grimm; Kenji Maillard; Cédric Fournet; Catalin Hritcu; Matteo Maffei; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin (CoRR, 2017)

HACL*: A Verified Modern Cryptographic Library. - Jean Karim Zinzindohoué; Karthikeyan Bhargavan; Jonathan Protzenko; Benjamin Beurdouche (IACR Cryptol. ePrint Arch., 2017)

Verified low-level programming embedded in F. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (Proc. ACM Program. Lang., 2017)

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. - Niklas Grimm; Kenji Maillard; Cédric Fournet; Catalin Hritcu; Matteo Maffei; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin (CPP, 2018)

Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier. - Guido Martínez; Danel Ahman; Victor Dumitrescu; Nick Giannarakis; Chris Hawblitzel; Catalin Hritcu; Monal Narasimhamurthy; Zoe Paraskevopoulou; Clément Pit-Claudel; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; et al. (CoRR, 2018)

Meta-F ^ star : Proof Automation with SMT, Tactics, and Metaprograms. - Guido Martínez; Danel Ahman; Victor Dumitrescu; Nick Giannarakis; Chris Hawblitzel; Catalin Hritcu; Monal Narasimhamurthy; Zoe Paraskevopoulou; Clément Pit-Claudel; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; et al. (ESOP, 2019)

EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. - Tahina Ramananandro; Antoine Delignat-Lavaud; Cédric Fournet; Nikhil Swamy; Tej Chajed; Nadim Kobeissi; Jonathan Protzenko (USENIX Security Symposium, 2019)

Formally Verified Cryptographic Web Applications in WebAssembly. - Jonathan Protzenko; Benjamin Beurdouche; Denis Merigoux; Karthikeyan Bhargavan (IACR Cryptol. ePrint Arch., 2019)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cédric Fournet; Tahina Ramananandro; Aseem Rastogi; et al. (IACR Cryptol. ePrint Arch., 2019)

HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms). - Marina Polubelova; Karthikeyan Bhargavan; Jonathan Protzenko; Benjamin Beurdouche; Aymeric Fromherz; Natalia Kulatova; Santiago Zanella-Béguelin (CCS, 2020)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cédric Fournet; Natalia Kulatova; Tahina Ramananandro; et al. (SP, 2020)

A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. - Antoine Delignat-Lavaud; Cédric Fournet; Bryan Parno; Jonathan Protzenko; Tahina Ramananandro; Jay Bosamiya; Joseph Lallemand; Itsaka Rakotonirina; Yi Zhou 025 (IACR Cryptol. ePrint Arch., 2020)

HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms). - Marina Polubelova; Karthikeyan Bhargavan; Jonathan Protzenko; Benjamin Beurdouche; Aymeric Fromherz; Natalia Kulatova; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2020)

A modern compiler for the French tax code. - Denis Merigoux; Raphaël Monat; Jonathan Protzenko (CC, 2021)

FastVer: Making Data Integrity a Commodity. - Arvind Arasu; Badrish Chandramouli; Johannes Gehrke; Esha Ghosh; Donald Kossmann; Jonathan Protzenko; Ravi Ramamurthy; Tahina Ramananandro; Aseem Rastogi; Srinath T. V. Setty; Nikhil Swamy; Alexander van Renen; et al. (SIGMOD Conference, 2021)

Zero-cost meta-programmed stateful functors in F. - Jonathan Protzenko; Son Ho (CoRR, 2021)

Catala: a programming language for the law. - Denis Merigoux; Nicolas Chataing; Jonathan Protzenko (Proc. ACM Program. Lang., 2021)

Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations. - Son Ho; Jonathan Protzenko; Abhishek Bichhawat; Karthikeyan Bhargavan (SP, 2022)

Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version). - Son Ho; Jonathan Protzenko; Abhishek Bichhawat; Karthikeyan Bhargavan (IACR Cryptol. ePrint Arch., 2022)

TreeSync: Authenticated Group Management for Messaging Layer Security. - Théophile Wallez; Jonathan Protzenko; Benjamin Beurdouche; Karthikeyan Bhargavan (IACR Cryptol. ePrint Arch., 2022)

Aeneas: Rust verification by functional translation. - Son Ho; Jonathan Protzenko (Proc. ACM Program. Lang., 2022)

Comparse: Provably Secure Formats for Cryptographic Protocols. - Théophile Wallez; Jonathan Protzenko; Karthikeyan Bhargavan (IACR Cryptol. ePrint Arch., 2023)

Foundations of WebAssembly (Dagstuhl Seminar 23101). - Karthikeyan Bhargavan; Jonathan Protzenko; Andreas Rossberg; Deian Stefan (Dagstuhl Reports, 2023)

Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification. - Son Ho; Aymeric Fromherz; Jonathan Protzenko (Proc. ACM Program. Lang., 2023)

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator. - Antonin Reitz; Aymeric Fromherz; Jonathan Protzenko (CoRR, 2024)

Compiling C to Safe Rust, Formalized. - Aymeric Fromherz; Jonathan Protzenko (CoRR, 2024)

Sound Borrow-Checking for Rust via Symbolic Semantics. - Son Ho; Aymeric Fromherz; Jonathan Protzenko (Proc. ACM Program. Lang., 2024)

StarMalloc: Verifying a Modern, Hardened Memory Allocator. - Antonin Reitz; Aymeric Fromherz; Jonathan Protzenko (Proc. ACM Program. Lang., 2024)

Charon: An Analysis Framework for Rust. - Son Ho; Guillaume Boisseau; Lucas Franceschino; Yoann Prak; Aymeric Fromherz; Jonathan Protzenko (CAV (4), 2025)

TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security. - Théophile Wallez; Jonathan Protzenko; Karthikeyan Bhargavan (IACR Cryptol. ePrint Arch., 2025)