I am a researcher (directeur de recherche) at Inria, where I lead the Prosecco project ("Programming Securely with Cryptography") at INRIA Paris. I also teach part-time at Ecole Polytechnique and at the Master Parisien de Recherche en Informatique (MPRI). My research concerns the design and implementation of new program verification techniques that would enable formal analyses of large security-critical applications. My recent work focuses on using dependent type systems, such as F*. to investigate the (in)security of cryptographic protocols, such as TLS. A full list of my publications is available from my publications page. My work is primarily funded by an ERC Starting Grant, titled "CRYSP: Collaborative Cryptographic Security Proofs for Programs". I also receive some funds from the ANR AJACS grant on JavaScript security, and from the ERC H2020 Grant NEXTLEAP on privacy-preserving protocols for secure messaging.