Aeneas: Rust Verification by Functional Translation
summary
Aeneas translates a large, safe subset of Rust (no interior mutability or unsafe) into a pure lambda calculus so proofs avoid memory/address reasoning, implemented in Rust and OCaml and emitting backends for theorem provers. It defines a value-based, ownership-centric semantics for LLBC that enforces borrows via loans, approximates borrow graphs across calls using symbolic execution, and uses backward functions to propagate updates. The toolchain includes a compiler plugin (Calico) and proves a resizing hash table correct (first such Rust proof), but it currently omits unsafe, interior-mutable, and some language features.
AI-written summary · about
chapters (8)
- 0:00Context and C comparisons
- 1:09Understanding Rust borrows
- 3:36Verification frameworks
- 5:34Introduction to Aeneas
- 7:02The translation mechanism
- 10:01Modularity in design
- 11:41Framework architecture
- 13:23Limitations and future work
related talks
31mTowards a linear functional translation for borrowing
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
20mVerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…)
19mA Hybrid Approach to Semi-automated Rust Verification
50mRust's Borrow Checker Proven Correct!
40mRust’s approach of getting things right
18mVerus: Verifying Rust Programs using Linear Ghost Types
36mRust as a High-Level Langage