Aeneas: Bridging Rust to Lean for Formal Verification

As Rust continues its explosive growth across the software industry, organizations are recognizing that while Rust's memory safety guarantees are valuable, they may not be sufficient for critical systems. Rust programs can still panic, contain logic errors, or behave incorrectly despite being memory-safe—for many high-assurance applications, functional correctness is equally important as memory safety. Aeneas is a verification toolchain that translates Rust programs to several proof assistants, including Lean, enabling verification of functional correctness beyond what Rust's type system alone can guarantee.

Functional Translation: A New Approach to Rust Verification

Aeneas is developed by researchers Son Ho, Jonathan Protzenko and Aymeric Fromherz and was initially presented at ICFP 2022. A key goal of Aeneas’ development was to leverage Rust's rich type system to eliminate memory reasoning entirely for many Rust programs.

The key insight of Aeneas is to translate Rust's memory model and borrow semantics into a purely functional representation that can be reasoned about using proof assistants like Lean. This approach transforms the verification challenge from reasoning about complex memory operations to proving properties of pure functions - a task that Lean excels at.

How Aeneas Works with Lean

For Lean users, Aeneas generates Lean code that faithfully represents the original Rust program, but in a pure functional form that's amenable to formal verification. This representation preserves the semantics of Rust's borrow system without requiring reasoning about memory addresses or pointer arithmetic.

Aeneas targets Lean specifically because of its extensibility and flexibility. Unlike systems restricted to specific automation approaches, Lean allows the Aeneas developers to implement custom automation while providing excellent support for interactive proofs. This flexibility has for instance enabled the development of specialized tactics to efficiently reason about monadic programs generated by Aeneas.

Benefits for Organizations

For organizations considering formal verification of their Rust codebase, Aeneas with Lean offers several compelling advantages:

  • Simplified Verification: The pure, functional model generated by Aeneas eliminates the need for tedious memory reasoning, focusing verification efforts on functional correctness.

  • Clean Separation of Concerns: Aeneas enables extrinsic proofs where code and proofs are cleanly separated, allowing software engineers to focus on implementation while proof engineers handle verification independently.

  • Verify Code As-Is: No need to modify existing code or replace standard libraries with verification-specific alternatives—Aeneas extracts and works directly with the Lean model of your existing Rust code.

  • Extensible Framework: Leverage Lean's metaprogramming facilities and benefit from community efforts including libraries like Mathlib and improved automation tools.

Real-World Applications

While Aeneas is still evolving, it's positioned to play a significant role in high-assurance Rust development. Most notably, Aeneas is used in Microsoft's ongoing effort to port SymCrypt, the open-source cryptographic library used in Windows, Azure, Xbox and other Microsoft products, from trusted C code to verified Rust code. Formal verification of this critical cryptographic code ensures both memory safety and functional correctness for algorithms that protect millions of users.

Next Steps

As Rust continues to gain adoption for systems programming, the need for formal verification tools will only grow. Aeneas represents a promising approach that leverages Lean's strengths in functional verification while respecting Rust's unique ownership and borrowing system.

For decision-makers considering formal verification strategies, Aeneas with Lean offers a path that combines the performance and safety benefits of Rust with the powerful reasoning capabilities of modern proof assistants.

To learn more about Aeneas: