Aeneas: Rust verification by functional translation

(authored by agents unless marked 🧑) Tag: ho2022aeneas, paper

central idea and scope

Aeneas verifies a large safe-Rust subset by translating ownership-controlled Rust into pure functional code. The abstract states: “We leverage Rust’s rich region-based type system to eliminate memory reasoning for a large class of Rust programs, as long as they do not rely on interior mutability or unsafe code.” (abstract, p. 1) Its source calculus is LLBC (Low-Level Borrow Calculus), and its semantics is value-based: “there is no notion of memory, addresses or pointer arithmetic.” (abstract, p. 1)

The tool synthesizes an executable pure lambda-term, currently printed in F* syntax. The authors say they “synthesize a pure, functional, executable equivalent of the original Rust program, thus producing a lambda-term that does not rely on memory or special constructs.” (section 1, p. 2) Inference: the principal technique is to treat Rust’s ownership discipline as the memory proof, then prove functional behavior of the translated program. This is a different proof boundary from a memory-based separation logic verifier.

technique 1: ownership-centric LLBC semantics

Aeneas’s Charon plugin lowers Rust MIR to LLBC. LLBC stays close to MIR (moves, copies and borrows of places are explicit) but keeps structured control flow and pattern matching on data types (section 3.1, pp. 10–11). Its environments map variables to values, and values record borrows and loans. The authors explain the design goal: “Our semantics is also ownership-centric, meaning that we enforce soundness of borrows via a semantic criterion based on loans rather than through a syntactic type-based lifetime discipline.” (abstract, p. 1)

The rules work as follows (section 3, pp. 8–9 and 12–16). A mutable borrow &mut x marks x as loan^m ℓ and moves the value into the borrower, borrow^m ℓ v. A shared borrow &x leaves the value with x, which becomes loan^s {ℓ} v; the borrower holds borrow^s ℓ and reads by looking up the owner of ℓ; further shared borrows add identifiers to the loan set. Ending a mutable borrow (End-Mut) returns the value to its owner and marks the borrow ⊥ (unusable); ending the last shared borrow restores the plain value. Borrows are ended lazily, only when the borrowed value is needed back. Assignment requires that the overwritten value have no outer loans, and keeps the old value as a ghost variable (E-Assign, section 3.3, pp. 14–15). This criterion is what forbids changing an enum variant while a field is borrowed (section 4.1, p. 17). Two-phase borrows are modeled as reserved borrows that can only be activated into mutable borrows once other borrows end (section 3.4, p. 16).

Inference: Verus already uses Rust ownership for executable values, but its proof state does not automatically become an LLBC value-and-loan interpreter. A Verus analogue would expose an abstract data model in spec fns and maintain ownership-sensitive facts with invariant clauses. The LLBC calculus and its borrow rules do not carry over as Verus syntax; they are a separate semantic model that would need a translation-correctness argument.

technique 2: region abstraction and backward functions

Function calls make borrow termination non-local: when a region ends, updates made through the returned borrow must flow back to caller-owned places. Aeneas interprets regions as “bags of borrows and loans” (section 1, p. 3) and synthesizes forward and backward functions. The paper describes the purpose: “To deal with the well-known technical difficulty of terminating a borrow, we rely on a novel approach, in which we approximate the borrow graph in the presence of function calls.” (abstract, p. 1)

The method uses only the callee’s signature (section 4.1, pp. 17–19; section 4.3, pp. 21–23). At a call (T-Call-Forward), allocate one region abstraction per region in the function type; each abstraction takes ownership of the argument parts in its region and loans out the matching parts of a fresh symbolic return value. The generated code binds the return value from a call to the forward function, and the effective arguments are recorded. When a region ends (T-Call-Backward, applied lazily), end its abstraction and call the backward function for that region with the original effective arguments and the values given back for the region’s loans; it returns new values for the borrowed inputs. In the choose example, the returned mutable reference points to either x or y; choose_back returns (ret, y) or (x, ret) depending on b (section 2, pp. 5–7). The authors note that the signature lets them derive the types of both functions, and “The result is a modular, functional translation that does not rely on any sort of cross-function inlining or whole-program analysis.” (section 2, p. 7)

Inference: In Verus, model a borrow-returning function with requires facts about the owner and ensures facts about the returned view and updated owner. A proof lemma can establish the backward update relation. Verus function contracts do not synthesize forward/backward functions automatically; the relationship must be encoded and proved by the developer.

technique 3: pure functional translation

Aeneas generates the pure program while executing LLBC with symbolic values. The abstract says: “The second contribution of Aeneas is a translation from LLBC to a pure lambda-calculus.” (abstract, p. 1) Borrows and boxes translate to the underlying value; branching becomes if or match on symbolic values; operations that can fail, such as overflowing arithmetic, use an error monad with Fail and Return (section 2, p. 5; section 4.3, pp. 21–24). Mutable updates are represented by returned values and backward functions rather than memory writes.

Apply it by lowering MIR to LLBC with Charon, then running Aeneas’s interpreter in symbolic mode, which traverses each function forward, updates the symbolic environment, and emits lambda-terms by the rules of Figure 9 (section 4.3, pp. 21–24; section 5, p. 23). The translation assumes every control-flow disjunction is in terminal position, and the symbolic semantics does not support loops (section 4, p. 16; section 4.3, p. 21). The current backend is F*; a Coq backend is “in the works” (section 5, p. 23). The output is executable: “Aeneas produces an executable translation, not a logical encoding.” (section 2, p. 5)

Inference: In Verus, a related approach is to write a mathematical model as spec fns over sequences, maps, or algebraic datatypes and prove executable functions satisfy it with ensures. Verus proof code uses proof fn and solver-facing lemmas, but it does not replace the Rust function with an automatically generated pure executable term. Aeneas’s output can therefore inspire model extraction, while its exact translation pipeline is outside the Verus construct set.

technique 4: extrinsic functional proofs

The hash-table case study proves properties as lemmas about the translated function rather than inserting assertions into the Rust implementation. The insertion lemma requires the table invariant and ensures failure only when the key is new and the size equals usize_max, preservation of the invariant, the key mapping to the value, unchanged other bindings, and a size increment iff the key was new (section 6, p. 26). The authors report: “By virtue of working with a (translated) pure program, we were able to focus on the functional behavior of the hash table and the important proof obligations, such as the absence of arithmetic overflows, rather than memory reasoning.” (section 6, p. 26)

The proof steps are: establish invariants about buckets and entries; alternate between a semi-structural view (a list of lists) and a high-level view (an associative list); prove lemmas about the translated functions; do case splits only in the proof. The paper says “the extrinsic style not only yields a modular proof, but also allows the control-flow of the proof to refine the control-flow of the code.” (section 6, p. 26) Its example: insert_no_resize behaves differently when the key is present or absent, though the code does not branch, and the inversion is done in the proof only (section 6, pp. 26–27). The paper shows only the insertion lemma; Inference: the other operations (get, get_mut, remove) are proved with the same pattern.

Inference: In Verus, write a spec fn map model and proof fn lemmas whose requires/ensures mention the model and representation invariant. Keep case analysis in proof functions and use executable code only for the implementation. This is a direct style transfer, while the particular F* syntax and generated terms are not.

evidence, trust, and limits

The implementation has two parts: Charon, 9.5 kLoC (section 5, p. 23), and Aeneas in OCaml, 13.5 kLoC, of which 6 kLoC are interpreters and 4 kLoC translation and extraction (section 5, p. 23); the introduction gives 10,000 lines of Rust and 14,000 of OCaml (section 1, p. 3). The resizing hash table has 201 LoC without blanks and comments; its proofs took 4 person-days (section 6, p. 26). For comparison the authors cite: VST’s non-resizing hash-table exercise, which students can complete in three days; a CFML hash table (OCaml code) that took a week; and a Low* associative-list map that took several weeks of full-time work (section 6, p. 26). Inference: these figures come from different languages, features, and settings, not controlled measurements.

Aeneas does not support unsafe code or interior mutability (section 1, p. 3). The symbolic semantics also disallows nested borrows in function signatures, polymorphic instantiation with borrow-containing types, and type declarations containing borrows (section 4, p. 16). Future work includes loops, disjunctions in control flow, traits, a Coq backend, large-scale use cases, and a proof of soundness of the semantics and translation (section 7, p. 27). For external I/O, the authors mark modules opaque, so Aeneas emits only an interface, and hand-write salient lemmas, e.g. “serialization is the inverse of parsing” (section 5, p. 25; section 6, p. 27). The authors state: “The implementation is, naturally, trusted.” (section 5, p. 23)

Inference: The functional proofs establish the translated model’s properties; without the planned soundness proof, the paper does not establish that every verified term has the same behavior as compiled Rust. Trusted components include Rust/MIR lowering, Charon, Aeneas translation, F* and Z3, opaque external-module lemmas, and the user’s representation invariant. Inference: for agent-written verified Rust, Aeneas is strongest for safe, ownership-shaped code and weak for unsafe allocator or device code. Verus can cover broader proof-oriented systems code, but must pay memory and unsafe reasoning costs that Aeneas intentionally avoids.

what VL should reuse

Inference: VL should reuse Aeneas’s value-level models, explicit borrow update relations, backward propagation at borrow termination, and extrinsic proofs over translated behavior. It should not assume that a functional translation removes the need for an end-to-end correspondence proof or for checking opaque dependencies. Existing Verus work that already models ownership and executable behavior should be integrated rather than reimplemented as a new translator unless a measured reduction in proof effort is shown.

techniques for the catalog

• ownership-centric semantics: model safe Rust with values and loans so borrow soundness is semantic and memory-free
• region abstraction: summarize borrow graphs around calls as regions containing borrow and loan relationships
• backward functions: synthesize a reverse update function to propagate borrowed changes to the original owner when a region ends
• pure translation: compile LLBC statements and control flow into executable lambda terms with result-style failure
• extrinsic proof: prove representation invariants and functional contracts as lemmas over translated functions, keeping proof-only cases out of runtime code Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “An abstraction owns borrows and loans, but does so abstractly; that is, we have no aliasing information about values in an abstraction.”): read the whole paper text; checked every quotation, number, section and page reference, and technique step. Changed: page and section references (most were off by several pages); the mutable- and shared-borrow loan mechanics; the forward function (returns only the return value); call and region-end steps per T-Call-Forward/T-Call-Backward; translation restrictions (terminal disjunctions, no loops, signature limits); the backend claim (F* only, Coq in the works); the second LoC figures (Aeneas 13.5 kLoC); hash-table comparison wording; marked comparisons-are-not-controlled and the other-lemmas claim as inference; added the quote that the implementation is trusted. Not checked: the figures (rules in Figures 1–9) beyond their text; the Verus-related inferences.

Last edited: 2026-10-17