Aymeric Fromherz: Aeneas: Formal Verification of Rust programs by Functional Translation

Please join us for a talk by Aymeric Fromherz on the formal verification of Rust programs.

Title: Aeneas: Formal Verification of Rust programs by Functional Translation
Speaker: Aymeric Fromherz (Inria)
When: Wednesday, April 30 2025, 16:00–17:00
Where: Room PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy

Abstract: The Rust programming language has recently gained traction in industrial settings and in the systems community. A large part of this success stems from several key features of the language: Rust provides both the high performance and low-level idioms commonly associated to languages like C and C++, as well as memory safety by default thanks to its rich, borrow-based type system. However, despite being safer than C or C++, Rust programs are not immune to bugs and vulnerabilties, including aborted executions (i.e., Rust’s panic), incorrect uses of the unsafe escape hatch, or simply programs that do not match their expected behaviour, raising the need for novel static analyzers and verification tools.

To this end, we present Aeneas, a new toolchain geared towards the formal verification of Rust programs. Aeneas leverages Rust’s region-based type system to eliminate memory reasoning for a large class of Rust programs: relying on a custom borrow-centric symbolic execution, the toolchain translates safe Rust programs to a semantically equivalent functional model in proof assistants such as Lean, Rocq, or F*, enabling the use of powerful logics to specify and reason about programs.

In this talk, we will show the core ideas behind Aeneas’ functional translation on several examples, and present the broader ecosystem around Aeneas, including the Charon analysis framework and ongoing work on transpilers between C and Rust to handle legacy systems.

About the speaker: Aymeric Fromherz is a researcher in the Prosecco team at Inria Paris. His research aims to develop and apply tools to provide guarantees about critical software. A large part of his work focuses on the development of verified, high-performance cryptographic primitives using the F* proof assistant, such as the HACL* library that he co-maintains. His other recent projects aim to apply formal verification techniques to Rust programs through the Aeneas framework, as well as developing tools to establish the safety of computational law implementations as part as the AVoCAT project that he co-leads. He received his PhD from Carnegie Mellon University in 2021.