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.

翻译：Rust编程语言提供了一种强大的类型系统，用于检查线性性和借用规则，使代码能够在无需垃圾回收的情况下安全地操作内存，这使得Rust成为开发底层高可信系统的理想选择。对于此类系统，形式化验证有助于证明超越类型安全的功能正确性属性。本文提出Verus——一种基于SMT求解器的Rust程序形式化验证工具。使用Verus时，程序员通过Rust语言表达证明和规约，使证明能够利用Rust的线性类型和借用检查机制。我们展示了如何利用这一特性操作线性类型权限，让Rust代码安全地管理内存、指针和并发资源。Verus通过一种新颖的模式系统组织证明和规约，该系统将不进行线性性与借用检查的规约，与需要检查线性性和借用性的可执行代码及证明区分开来。我们通过一个小型lambda演算形式化了Verus的线性性、借用机制和模式系统，并证明了该演算中规约与证明的类型安全性和可终止性。最后通过一系列示例验证Verus的实际应用能力，包括指针操作代码（基于异或的双向链表）、具有内部可变性的代码及并发代码。