Aeneas: Rust Verification by Functional Translation

Motivation

• Rust’s ownership discipline prevents arbitrary aliasing, but its rich borrow mechanisms make verification technically difficult.The relevant mechanisms include reborrows, two-phase borrows, and functions returning borrows.Source: §1 · p. 2

Implementation

• Aeneas emits pure code for theorem provers and is designed to support multiple backends, including F∗ and prospective Coq, Lean, Viper, and Why backends.The implementation combines Rust and OCaml, with 10,000 and 14,000 lines of code respectively, excluding comments and whitespace.Source: §1 · pp. 2–3

Approach

• Aeneas replaces memory-oriented reasoning with a pure functional translation for Rust programs that avoid unsafe code and interior mutability.The approach treats references primarily as performance or representation mechanisms when ownership already enforces a strong discipline.Source: §1 · pp. 2–3

Semantics

• LLBC provides a value-based, ownership-centric semantics that tracks loans and aliasing without memory, addresses, or pointer arithmetic.Its semantic ownership criterion is intended to capture borrowing beyond the Rust compiler’s current syntactic lifetime discipline.Source: §1 · p. 3

Translation

• Region abstraction approximates borrow graphs across function calls, enabling backward functions to handle borrow termination without prophecy variables or after clauses.This supports a modular translation based on function structure rather than cross-function inlining or whole-program memory reasoning.Source: §1 · pp. 2–3

Evaluation

• Evaluation spans feature-completeness micro-benchmarks and a resizable hash table, reporting substantial verification-productivity gains.The authors emphasize fewer memory-specific proof obligations, lightweight integration with existing projects, and freedom to choose a productive verification framework.Source: §1 · pp. 3–4

Mutable Borrows, Functionally

• Aeneas translates reference-manipulating Rust into pure code because Rust’s ownership guarantees make the references unnecessary for functional reasoning.The translation preserves error behavior such as failure on integer overflow.Source: §2 · p. 5

Returning a Mutable Borrow, and a Backward Function

• A mutable reference call can require a backward function that propagates updates from the returned borrow back to the originally borrowed variables.The forward function handles the call, while the backward function runs when the associated region terminates.Source: §2 · p. 6
• The choose example uses choose_fwd for the call and choose_back to restore ownership of x and y after updating the selected result.The backward function returns the modified value to the branch selected by b while leaving the other input unchanged.Source: §2 · p. 6
• Backward functions are derived from a function signature, allowing modular translation even when the callee’s computational body is opaque.This avoids cross-function inlining and whole-program analysis by reversing the relevant ownership transfers.Source: §2 · p. 7

Recursion and Data Structures

• For recursive list access, Aeneas pairs list_nth_mut_fwd with list_nth_mut_back to modify an element and rebuild the list during backward propagation.The backward function follows the forward control flow and constructs new Cons cells as recursive updates return.Source: §2 · pp. 7–8
• The examples also translate immutable list traversal and executable unit tests, with the prover discharging the test assertion directly through normalization.The list example supports regaining list ownership after mutation and checking that the resulting sum is seven.Source: §2 · pp. 5, 7, 8

3 AN OWNERSHIP-CENTRIC SEMANTICS FOR RUST

• The semantics precisely tracks Rust ownership and aliasing through loan identifiers and an ownership-centered environment, simplifying reasoning by focusing on borrowed values through their owners.Mutable borrows transfer exclusive ownership, while shared borrows permit multiple read-only aliases whose loans must all terminate before ownership is regained. The formalism intentionally excludes unsafe blocks and is designed for non-unsafe Rust programs.Source: §3 · p. 9
• The semantics uses lazy, on-demand borrow reorganization to regain ownership only when needed, enabling forward evaluation and explaining borrowing errors through unusable terminated references.This approach preserves precise aliasing information for reborrowing and reaches the same semantic conclusion as rustc, though it may report the error at a different location.Source: §3 · pp. 10–11

3.1 The Low-Level Borrow Calculus

• LLBC models Rust programs close to MIR while retaining structured control flow, pattern matching, pure data construction, and explicit move, copy, and borrow operations.Its central place construct combines a base variable with field offsets and indirections, and assignments or returns target places.Source: §3.1 · p. 11

3.2 A Structured Memory Model

• The structured memory model represents stores exclusively as variable-to-value environments, supporting fine-grained reads and writes through paths without memory addresses or pointer arithmetic.Reads follow paths through mutable or shared borrows, while writes update only the selected subexpression and are permitted through mutable borrows or boxes.Source: §3.2 · pp. 11, 14

3.3 Semantics of Ownership and Borrows

• Operational rules make ownership transfer explicit: mutable borrows create exclusive loans, shared borrows add tracked loans, moves require unloaned values, and copies manage shared reborrowing.Ghost updates perform bookkeeping without runtime effects, and reserved borrows account for Rust’s two-phase borrows.Source: §3.3 · pp. 14–17
• Assignments require ownership of the right-hand value and forbid overwriting values containing outer loans, preserving safety under ownership.The old value is retained as an inaccessible ghost value so useful ownership knowledge is not discarded.Source: §3.3 · p. 17

3.4 Reorganizing Environments and Terminating Borrows

• Borrow termination is modeled declaratively and lazily through environment reorganization before and after statements, without explicitly modeling MIR drop nodes.Reorganization uses rewriting rules over environments and terminates borrows only when the borrowed value must be recovered.Source: §3.4 · pp. 17–18, Figure 9 · p. 18
• Reserved borrows model two-phase borrows: they cannot be copied, dereferenced, or written, and activate as mutable borrows only after other borrows end.The rules require unique ownership for termination, precisely capturing reborrow constraints; shared borrows become unusable and mutable borrows return the value to its owner.Source: §3.4 · p. 18

4 SYMBOLIC ABSTRACTIONS AND FUNCTIONAL TRANSLATION

• Region-centric symbolic semantics abstracts function-call effects while retaining sufficient ownership and aliasing information to generate a functional translation.Region abstractions own consumed borrows and produced loans abstractly, transferring ownership back when terminated.Source: §4 · p. 19, §4.1 · p. 20
• This symbolic semantics supports recursive functions but excludes loops, nested borrows in signatures, borrow-containing polymorphic instantiations, and borrow-containing type declarations.The authors state that most restrictions may be addressed through additional engineering and discuss them in Section 7.Source: §4 · p. 19

4.1 Symbolic Semantics by Example

• Symbolic execution refines unknown values through matches and prevents invalid enum updates by requiring outstanding outer loans to be terminated first.Borrowing refined option fields preserves alias precision, while terminating a borrow can invalidate further use of its pointer.Source: §4.1 · pp. 19–20
• For calls spanning multiple regions, input, loan, and output-borrow projectors distribute arguments and returned components according to region ownership.Projectors decompose tuples and retain only components belonging to each enclosing region.Source: §4.1 · pp. 21–22, §4.2 · p. 22

4.2 From Concrete to Symbolic Semantics

• The formal symbolic semantics extends the concrete system with symbolic values, three projector kinds, and rules for unfolding, folding, and safely ending abstractions.Ending an abstraction requires no outstanding loans or loan projectors, then returns borrows with fresh symbolic values to ghost variables.Source: §4.2 · pp. 22, 24

4.3 From Symbolic Semantics to Functional Code

• Aeneas generates pure functional code by symbolically executing LLBC while synthesizing an AST, with symbolic values becoming runtime let-bound variables.The translation assumes every control-flow disjunction is terminal, requiring continuation duplication to avoid the join problem.Source: §4.3 · p. 24, §4.3.1 · p. 24

4.3.1 Translation Example: Forward Function.

• The forward translation handles a call by introducing a region abstraction, projecting effective arguments into it, and pairing forward calls with symbolic return-value projectors.Borrow types translate to identity, so the synthesized call is monadic and operates on the translated arguments directly.Source: §4.3.1 · p. 25
• In the forward example, ending the region abstraction invokes choose_back with the original arguments and the updated return value, producing the values restored to the caller.The generated function ends the borrow and returns the synthesized result after inlining unnecessary bindings.Source: §4.3.1 · pp. 26–27

4.3.2 Translation Example: Backward Function

• Backward function initialization uses an abstraction containing caller-owned loans and output borrow projectors, dualizing the caller’s view of borrowed arguments.The synthesized function adds a ret parameter representing the value supplied when the associated region ends.Source: §4.3.2 · p. 27
• Backward translation models caller-updated mutable borrows by replacing returned symbolic values and ending loans to propagate updates back to original owners.The backward function receives the original arguments and a return value, then closes input abstractions to produce the values returned to the caller.Source: §4.3.2 · p. 28
• The synthesis judgment traverses statements forward, generating pure lambda terms or continuation contexts while updating symbolic environments and translation metadata.Continuation-passing style implements expressions with holes; source variables are represented through symbolic values rather than directly copied into the target calculus.Source: §4.3.3 · p. 28

4.3.3 Synthesis Rules.

• Function calls allocate region abstractions and return-value symbols, while lazily synthesized backward calls terminate abstractions and reconstruct values returned to the caller.Forward calls record effective arguments and loans; backward calls use those arguments and terminated projector loans to compute restored symbolic values.Source: §4.3.3 · p. 29
• Symbolic matches either select a statically known branch or refine an unknown scrutinee into constructor values with fresh field symbols, preserving lexical binding and sound borrow tracking.This precise substructural refinement prevents loss of borrow-checking precision and avoids permitting type-incorrect programs.Source: §4.3.3 · pp. 29–30

Implementation pipeline

• Charon translates Rust MIR into LLBC, reordering definitions, reconstructing data types, grouping mutual recursion, and removing overly low-level idioms before emitting a JSON AST.Charon is implemented as a Rust compiler plugin and contains 9.5 kLoC.Source: §5 · p. 30
• Aeneas interprets the Charon-generated AST concretely to produce values or symbolically to produce translated programs, currently extracting to F* with Coq, HOL4, and Lean planned.The symbolic interpreter also acts as a borrow checker using Aeneas’s semantic notion of borrows.Source: §5 · p. 30

Trust and performance

• The implementation comprises 13.5 kLoC of Aeneas plus 9.5 kLoC of Charon, with extensive invariant checks that make processing take a few seconds per file.The checked invariants include well-typed environments, consistent borrows, and the absence of mutable loans in shared values.Source: §5 · pp. 30, 32

Supported features

• Recursive translations emit F* decreases annotations linked to user-maintained termination lemmas, while the planned Coq backend will use user-controlled fuel parameters.This preserves a workflow in which generated files reference separate lemma files maintained by users.Source: §5 · p. 32
• Aeneas supports opaque modules and external dependencies through generated interfaces, allowing users to provide lemmas that characterize external functions without wrappers for the entire Rust standard library.Its combined world-and-error monad lets users state assumptions about the external world modularly and provides a lightweight monadic effect system.Source: §5 · pp. 32–33

• The hash table supports insertion, immutable and mutable lookup, removal, linked-list buckets, automatic resizing, polymorphic values, and fixed usize keys.The proofs do not rely on the fixed key type, and generic keys are planned once traits are supported.Source: §6 · p. 33
• The proof establishes that insertion updates the selected binding, preserves other bindings, and treats resizing as functionally identity while checking overflow and mutable in-place updates.The proof uses invariants for pairwise-disjoint keys and correct hashing, switching between list-of-lists and flattened associative-list views.Source: §6 · pp. 33–34
• Aeneas’s pure translation supports extrinsic, modular proofs that avoid memory reasoning, modifies-clause lemmas, and separation-logic framing tactics.Proof control flow can refine code behavior without adding runtime branches or assertions, as illustrated by insert_no_resize.Source: §6 · p. 34
• Four person-days verified a 201-LoC resizable hash table, and comparisons led the authors to call Aeneas very competitive with established frameworks.The comparison included a three-day VST exercise for a non-resizing table and one week for a CFML verification.Source: §6 · p. 34
• Compared with a Low* imperative-map verification requiring several weeks of full-time work, the authors claim Aeneas vastly improves the state of the art for low-level F∗ verification.This comparison concerns another data structure verified in Low*, the subset of F∗ that compiles to C.Source: §6 · p. 34
• Aeneas accepts a mutable-borrow example rejected by the current Rust checker because its symbolic, semantic loan discipline is not lexical.The get_suffix_at_x example requires ending reborrows after the conditional; Polonius accepts it, but its status is described as unclear.Source: §6 · pp. 34–35
• Aeneas models I/O and external dependencies with opaque modules, state types, module signatures, and a state-error monad.Users can supply models or assumptions for generated declarations without revealing external implementations.Source: §6 · pp. 35–36
• Aeneas accepts additional precise-reborrow examples that Rust’s current checker and Polonius reject, although the authors describe these cases as anecdotal and probably impractical.The semantics does not retain hierarchy links between certain reborrows, allowing later accesses that the borrow checkers reject.Source: §6 · pp. 36–38

Planned extensions

• Support for loops, control-flow disjunctions, traits, a Coq backend, and large-scale use cases remains planned future work.The authors characterize these additions as engineering tasks.Source: §7 · pp. 38–39

Soundness and borrow checking

• A future soundness proof could establish Aeneas as an alternate Rust borrow checker and inform future borrow-checker evolution.The proposed comparison targets include Stacked Borrows and RustBelt.Source: §7 · p. 38

Language features

• Function pointers and closures are expected to fit the approach, while adding traits is described as mostly an engineering task.Functions are characterized by a forward function and backward functions for region variables.Source: §7 · p. 38

Nested borrows

• Nested mutable borrows across different regions remain conservatively restricted because borrow overwrites are difficult to represent symbolically.The difficult case is exemplified by types such as &'a mut &'b mut T.Source: §7 · p. 38

Region abstractions

• Borrow abstractions can become too imprecise during chained calls, causing symbolic execution to get stuck and motivating finer-grained subregion abstractions.The current region abstractions are described as too monolithic for the reported example.Source: §7 · p. 38

Nested borrows

• Nested mutable borrows appear rarely exploited in practice because many cases can be split into non-nested input borrows.The authors plan to investigate whether real use cases depend on this feature.Source: §7 · p. 39

Borrow-containing types

• Borrow-containing algebraic data types and type-parameter instantiations are unsupported because they require backward types and higher-order backward functions.The authors identify substantial engineering effort as the barrier to supporting these cases.Source: §7 · p. 39

Functional translation

• Electrolysis also translates Rust to a pure lambda calculus, but uses lenses, imposes stronger restrictions, and lacks a formal model of semantic correctness.Electrolysis targets Lean and, for example, restricts functions returning borrows to their first argument.Source: §8 · p. 39

RustBelt

• RustBelt complements Aeneas by handling soundness and unsafe Rust through Iris, whereas Aeneas targets larger amounts of safe Rust without that full framework.The two systems address different scales and safety settings.Source: §8 · p. 39

Logical encodings

• RustHorn and RustHornBelt encode Rust programs logically and address soundness through non-mechanized or mechanically proved connections to Rust semantics.Aeneas plans to investigate a similar proof style for its ownership-centric semantics.Source: §8 · p. 39

Automated verification

• Creusot and Prusti emphasize automated intrinsic proofs using annotations, SMT, or Viper, while Aeneas instead generates a trusted pure translation for extrinsic proofs.Creusot’s dedicated encoding is reported to outperform the general-purpose Prusti frontend in verification performance.Source: §8 · pp. 39–40

Permission-based systems

• RefinedC and Aeneas both avoid backtracking, but RefinedC relies on permission-based memory reasoning whereas Aeneas uses Rust borrows to lazily terminate borrows.Aeneas’s backward functions play a role comparable to Heapster’s reachability permissions, whose generation Aeneas automates with Rust’s borrow discipline.Source: §8 · p. 40

Cogent

• Cogent produces C, Isabelle/HOL specifications, and per-compilation refinement proofs, but its linear type system is less expressive than Rust’s and lacks an equivalent of mutable borrows.Unlike Cogent, Aeneas enables integration with existing developments through a generated pure translation.Source: §8 · p. 40

Conclusion

• Aeneas targets safe Rust with extrinsic reasoning, aiming for a lightweight functional encoding that supports proof-engineering productivity.Figure 14 compares tools by their target programs and toolchains.Source: §8 · p. 41