I am a Researcher in the RiSE group at Microsoft Research Redmond, which I joined in Fall 2014. Previously, I was 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.

My research now focuses on formally verifying critical software, i.e. showing with mathematical certainty that the software has no bugs and exhibits the intended behavior. To that end, I use the F* programming language, and its new Low* toolchain. It allows compiling a subset of F* programs to C for integration into existing software ecosystems. Code written in Low* and compiled by KReMLin has been integrated into Windows, Firefox, mbedTLS, and the Tezos blockchain, among others.

In addition to tooling, I work on the following software verification projects:

  • 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
  • miTLS, a verified implementation of QUIC and TLS 1.2/1.3 in F*, compiled to C

My work is part of the larger Everest Project, an ambitious research effort spanning three continents, five institutions and twelve timezones.

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.