We present Aeneas, a verification toolchain for Rust programs based on a
lightweight functional translation.
We leverage Rust's rich region-based type system to generate pure models for a large class
of safe Rust programs which can contain shared and mutable borrows, functions returning
borrows, traits and loops.
Doing so, we allow the user to reason about the original Rust program through the theorem
prover of their choice, and enable lightweight verification by eliminating memory
reasoning, allowing them to instead focus on *functional* properties of their code.
As of today, Aeneas has backends for F\*, Coq, HOL4 and most importantly Lean, for which
we are investing efforts to develop custom tactics and automation. Aeneas is currently
being used to verify optimised, low-level cryptographic code, that we will
present as well.
