I am a Principal Researcher in Azure Research. My research focuses on advancing the theory and practice of software verification, i.e. showing with mathematical certainty that a critical piece of code exhibits the intended behavior. As security and safety take the center stage, software correctness becomes even more consequential.

My joint work (with many wonderful collaborators!) has received the Internet Defense Prize, and our code has made it into BoringSSL, the Linux kernel, the Python programming language, and the Firefox web browser, among others. My research on verified cryptography was featured in Quanta Magazine and IEEE Computer Magazine; my research on computational law appeared in Communications of the ACM, and received a SIGPLAN Research Highlight.

Previously, I was at Microsoft Research for 9 years, and before that, in the Gallium team at INRIA Paris from 2010 to 2014, designing and implementing Mezzo for my PhD under the direction of François Pottier.

Current projects

Rust verification (2022-). The future of verification lies with the Rust programming language. Aeneas is a new verification frontend that allows the programmer to verify safe Rust code via a functional translation. See the paper intro for a manifesto. Eurydice compiles Rust to C, allowing programmers to write their code in a modern, easy-to-verify language, while still targety legacy environments and toolchains. Scylla is an experimental tool that can rewrite regular, well-behaved C code to safe Rust automatically.

Verified Protocol Stacks (2019-). Security protocols are pervasive in modern communication software, yet true end-to-end verification results for real-world protocols remain elusive. New developments:

  • Noise*, a protocol compiler, proven correct and secure once and for all – we generate 59 protocol stacks “for free”, complete with state machine and peer management, in C.
  • MLS*, a hybrid JS/WebAssembly implementation of the MLS protocol with security proofs (Internet Defense Prize).
  • Signal*, a provably secure implementation of the Signal protocol, including compilation the Web via WebAssembly.

The Low* toolchain (2016-2022) compiles F* programs to C. Code written in Low* has been integrated into Windows, Firefox, mbedTLS, and the Tezos blockchain, among others. I co-lead several verified software libraries which use Low*, such as:

  • EverCrypt, a complete cryptographic library that offers abstraction, multiplexing, agility and CPU auto-detection, verified in F*, compiled to C and assembly
  • HACL*, a collection of verified cryptographic algorithms, verified in F*, compiled to C
  • EverQUIC, a verified implementation of the QUIC record layer, complete with a proof of cryptographic security

The Low* strand of work is gradually transitioning towards industrial support & impact. I advise Cryspen, a startup that provides commercial support for HACL* and other projects.

Formal Computational Law (2020-2022) I studied how the tools & techniques of formal methods and PL can shed light on some thorny corners of the law. See Catala, and see Talks for an overview of this research program. My student Denis Merigoux is carrying the torch.

Open-source (2009-). In my spare time, I maintain several open-source projects, including a Thunderbird addon that is now the 4th most-used addon with 200,000 users.

More information on the research and software pages.

Students

  • Théophile Wallez (2021-), co-advised with Karthik Bhargavan at INRIA
  • Son Ho (2020-2024), co-advised with Karthik Bhargavan at INRIA, GDR-Sécurité PhD Award (shortlisted). Son is now a post-doc at Microsoft Research.
  • Denis Merigoux (2018-2021), co-advised with Karthik Bhargavan at INRIA, Gilles Kahn PhD Award. Denis is now a junior researcher at INRIA.

News

  • 2024/08: post-quantum crypto compiled by Eurydice from Rust to C makes it into BoringSSL, Firefox, and others
  • 2024/08: co-chairing VSTTE with Azalea Raad
  • 2023/08/09: thrilled to receive the Internet Defense Prize and a Distinguished Paper Award at Usenix Security!
  • 2023/07/06: our paper on the proof engineering powering HACL*, accepted at ICFP’23 (preprint)
  • 2023/05/09: I will be giving a keynote at HCSS’23.
  • 2023/03/12: thrilled to participate in this year’s POPL programm committee
  • 2023/02/06: verified cryptography from HACL* in Python!
  • 2023/02/03: excited to be on a panel, for “What’s the Big Idea: Law and Our Technological Future”
  • 2023/01/09: my student Denis Merigoux won the Gilles Kahn PhD award. Congratulations, Denis!
  • 2022/10/18: New edition of ProLaLa, which I am once again co-organizing. Send us your finest and freshest work!
  • 2022/01/30: CACM publishes an article about computational law which features Catala prominently

Recent blog entries

subscribe via RSS