I am on leave from Inria, working as co-founder and chief research scientist at Cryspen.

My research concerns the design and implementation of program verification techniques that would enable the formal analyses of real-world security protocols and cryptographic software. A full list of my publications is available from DBLP. My CV is available here.

I have recently been involved in the design, analysis, and standardization of TLS 1.3, Hybrid Public Key Encryption, and Messaging Layer Security at the IETF.

Recruitment: At Cryspen, we are looking for both crypto and proof engineers who are excited about building high-assurance cryptographic software using formal analysis techniques. At Inria, my old team Prosecco is always on the lookout for excellent Ph.D. students and Post-Docs to work on a variety of topics, including cryptographic protocol design, analysis, and implementation.

Current Projects: Cryspen, hax, libcrux, bertie, DY*, hacspec, F*

Past PhD Students: Evmorfia-Iro Bartzia, Antoine Delignat-Lavaud, Jean Karim Zinzdohoue, Nadim Kobeissi, Benjamin Beurdouche, Marina Polubelova, Natalia Kulatova, Denis Merigoux, Benjamin Lipp, Son Ho, Théophile Wallez

News: (See the Cryspen blog for more recent updates.)