FLEXTLS: A Tool for Testing TLS Implementations. - Benjamin Beurdouche; Antoine Delignat-Lavaud; Nadim Kobeissi; Alfredo Pironti 001; Karthikeyan Bhargavan (WOOT, 2015)

A messy state of the union: taming the composite state machines of TLS. - Benjamin Beurdouche; Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Markulf Kohlweiss; Alfredo Pironti 001; Pierre-Yves Strub; Jean Karim Zinzindohoue (Commun. ACM, 2017)

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

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)

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)

Formal Verification for High Assurance Security Software in FStar: Application to communication protocols and cryptographic primitives. (Vérification formelle de logiciels de sécurité à haute assurance en FStar / Vérification formelle de logiciels de sécurité à haute assurance en FStar: Application aux protocoles de communication et aux primitives cryptographiques). - Benjamin Beurdouche (2020)

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

The Messaging Layer Security (MLS) Protocol. - Richard Barnes 001; Benjamin Beurdouche; Raphael Robert; Jon Millican; Emad Omara; Katriel Cohn-Gordon (RFC, 2023)

The Messaging Layer Security (MLS) Architecture. - Benjamin Beurdouche; Eric Rescorla; Emad Omara; Srinivas Inguva; Alan Duric (RFC, 2025)