一句话：提出 Aeneas，将 Rust 程序轻量翻译到纯 lambda 演算，免去内存推理并用定理证明器验证函数正确性。
Aeneas 是面向 Rust 的验证工具链，旨在让证明工程师摆脱内存推理、专注于功能性质。针对不含内部可变性与 unsafe 代码的 Rust 子集，作者为 LLBC（Low-Level Borrow Calculus）提出纯函数式、基于值且以所有权为中心的语义，用基于 loan 的语义准则而非语法生命周期保证借用可靠性。随后将 LLBC 翻译到纯 lambda 演算，并用后向函数与借用图近似处理函数调用下的借用终止，使用户可在任意定理证明器中推理原 Rust 程序。工具以 Rust 与 OCaml 实现；案例研究为可扩容哈希表，首次证明其功能正确性，并显示验证生产率显著提升。
We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. 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. Doing so, we relieve the proof engineer of the burden of memory-based reasoning, allowing them to instead focus on functional properties of their code. The first contribution of Aeneas is a new approach to borrows and controlled aliasing. We propose a pure, functional semantics for LLBC, a Low-Level Borrow Calculus that captures a large subset of Rust programs. Our semantics is value-based, meaning there is no notion of memory, addresses or pointer arithmetic. 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. We claim that our semantics captures the essence of the borrow mechanism rather than its current implementation in the Rust compiler. The second contribution of Aeneas is a translation from LLBC to a pure lambda-calculus. This allows the user to reason about the original Rust program through the theorem prover of their choice, and fulfills our promise of enabling lightweight verification of Rust programs. 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. This in turn allows us to perform the translation using a new technical device called backward functions. We implement our toolchain in a mixture of Rust and OCaml; our chief case study is a low-level, resizing hash table, for which we prove functional correctness, the first such result in Rust. Our evaluation shows significant gains of verification productivity for the programmer. This paper therefore establishes a new point in the design space of Rust verification toolchains, one that aims to verify Rust programs simply, and at scale. Rust goes to great lengths to enforce static control of aliasing; the proof engineer should not waste any time on memory reasoning when so much already comes “for free”!