Aeneas

Verify Rust programs in Lean while benefitting from a pure, functional model which abstracts away the memory! We are currently using Aeneas in the process of porting Microsoft’s open source cryptographic library, used in particular in Windows and Azure Linux, from trusted C code to verified Rust code - see Microsoft’s blog post. For more information about this project, including ongoing work and research topics for potential collaborations and internships, you can go here or on the official website.

Charon

Building tools which use the Rust compiler’s output, for instance to perform static analyses, is extremely tedious. If you do not want to waste time in boring engineering effort you can use Charon. Essentially, by calling charon cargo from within your crate, you get a file containing your serialized crate, in a high-level, easy to use AST. We also provide libraries in Rust and OCaml to deserialize this file, pretty print its components, etc. Charon is being used in several projects, including but not limited to Aeneas and the Eurydice compiler. The tool-paper provides a high-level overview of Charon’s features.

Past Projects

Dafny in Dafny

A partial formalization of the Dafny compiler within Dafny itself (github repo and workshop paper).

Noise*

A verified protocol compiler: give it the description of a protocol as input, and it produces a specialized, efficient implementation, shipped with a high-level API inspired by Wireguard, and backed by functional correctness and security proofs in F*. Every call to the compiler generates between 4k and 6k lines of low-level C code, and the compiler itself is implemented by using what is called a Futamura projection - a technique I would never have imagined to use in practice, and which is extremely powerful in combination with dependent types. More information here or in the S&P paper.

F* Extended Mode

The F* extended mode is a side project I did at some point to improve the interaction with F*, and in particular make the user less blind when writing proofs by inserting information about the context directly into their code. The principle is very simple: by calling dedicated commands, one could introduce the pre and post-conditions of an (effectful) function call, unfold definitions or split conjunctions in assertions. I merged the F* meta code necessary to compute this information to the F* main branch, but for some reason I never took the time to merge the elisp code into the F*-mode repo. I may find the motivation to do so in the future provided I get enoug traction.