一句话：提出基于 SMT 的 Verus，用线性 ghost 类型与模式系统验证 Rust 程序的功能正确性。
Rust 的类型系统通过线性与借用检查保证内存安全，但难以证明功能正确性。Verus 是一个基于 SMT 的 Rust 程序形式验证工具：程序员用 Rust 编写规范与证明，并利用线性类型和借用检查来操作线性 ghost 权限，从而安全地描述内存、指针与并发资源。其核心是新颖的模式系统，将不受线性/借用检查的规范与受检查的可执行代码和证明区分开。作者在小 λ 演算中形式化线性、借用与模式，并证明类型安全及规范/证明终止。案例包括 xor 双向链表、内部可变性与并发代码。
The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems. For such systems, formal verification can be useful to prove functional correctness properties beyond type safety. This paper presents Verus, an SMT-based tool for formally verifying Rust programs. With Verus, programmers express proofs and specifications using the Rust language, allowing proofs to take advantage of Rust's linear types and borrow checking. We show how this allows proofs to manipulate linearly typed permissions that let Rust code safely manipulate memory, pointers, and concurrent resources. Verus organizes proofs and specifications using a novel mode system that distinguishes specifications, which are not checked for linearity and borrowing, from executable code and proofs, which are checked for linearity and borrowing. We formalize Verus' linearity, borrowing, and modes in a small lambda calculus, for which we prove type safety and termination of specifications and proofs. We demonstrate Verus on a series of examples, including pointer-manipulating code (an xor-based doubly linked list), code with interior mutability, and concurrent code.
@article{paperbot2041,
title = {Verus: Verifying Rust Programs using Linear Ghost Types},
author = {Andrea Lattuada and Travis Hance and Chanhee Cho and Matthias Brun and Isitha Subasinghe and Yi Zhou and Jon Howell and Bryan Parno and Chris Hawblitzel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA1},
year = {2023},
doi = {10.1145/3586037}
}