Verus：验证 Rust 代码正确性的工具

# Verus 概览 - Verus 教程与参考 来源：https://verus-lang.github.io/verus/guide/ ## 键盘快捷键 按 ← 或 → 在章节间跳转 按 S 或 / 在书中搜索 按 ? 显示本帮助 按 Esc 隐藏本帮助 ## Verus 教程与参考 ## Verus 概览（https://verus-lang.github.io/verus/guide/#verus-overview） Verus 是一款用于验证 Rust 代码正确性的工具，其首要目标是对底层系统代码进行完整的功能正确性验证，并借鉴了以下现有验证框架的思想： [Dafny](https://github.com/dafny-lang/dafny)、[Boogie](https://github.com/boogie-org/boogie)、[F\*](https://github.com/FStarLang/FStar)、[VCC](https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/)、[Prusti](https://github.com/viperproject/prusti-dev)、[Creusot](https://github.com/xldenis/creusot)、[Aeneas](https://github.com/AeneasVerif/aeneas)、[Cogent](https://github.com/NICTA/cogent)、[Rocq](https://rocq-prover.org/)、[Isabelle/HOL](https://isabelle.in.tum.de/overview.html)。 验证是静态的：Verus 不会插入运行时检查，而是借助计算机辅助定理证明，静态地确保可执行的 Rust 代码在**所有可能执行路径**下都满足用户给出的规约。 具体而言，Verus 力求： - 提供一套**纯数学语言**来表达规约（类似 Dafny、Creusot、F\*、Coq、Isabelle/HOL） - 提供一套**基于经典逻辑**的数学语言来表达证明（类似 Dafny、F\*、Coq、Isabelle/HOL） - 提供一种**底层命令式语言**来编写可执行代码（类似 VCC），并基于 Rust（类似 Prusti、Creusot、Aeneas） - 生成**规模小、形式简单**的验证条件，使 [Z3](https://microsoft.github.io/z3guide/docs/logic/intro) 等 SMT 求解器能够高效解决，遵循以下原则： – 让数学规约语言尽可能贴近 SMT 求解器的数学语言（类似 Boogie） – 用轻量级**线性类型检查**而非 SMT 推理来处理内存与别名问题（类似 Cogent、Creusot、Aeneas 以及 [linear Dafny](https://github.com/secure-foundations/dafny/tree/betr/docs/Linear)） 我们认为 Rust 是实现这些目标的理想语言： Rust 在提供底层数据操作与手动内存管理的同时，拥有先进的高级安全类型系统，包括代数数据类型（带模式匹配）、类型类、一等函数等常见于高层验证语言的特性，使得规约与证明可以自然表达。更关键的是，Rust 的类型系统内置了复杂的线性类型与借用检查，可自动处理大部分内存与别名推理，因此剩余验证工作几乎可以忽略这些问题，把代码当作纯函数式程序对待，大幅降低验证难度。 目前，我们**不打算**： - 支持全部 Rust 特性与库（而是聚焦用户所需的高价值子集） - 自证验证器本身的正确性 - 验证 Rust/LLVM 编译器 ## 本指南（https://verus-lang.github.io/verus/guide/#this-guide） 本指南假设你已具备 Rust 基础。（若尚不熟悉，建议先花几个小时浏览 [Learn Rust](https://www.rust-lang.org/learn)。） 由于 Verus 直接沿用 Rust 语法与类型系统来表达规约、证明与可执行代码，因此没有独立的“规约语言”——所有规约和证明都用 Rust 语法编写并通过 Rust 类型检查。已掌握 Rust 的读者将更容易上手。 然而，验证 Rust 代码的正确性需要超出普通编程的概念与技巧。例如，Verus 通过宏扩展了 Rust 语法，引入 `forall`、`exists`、`requires`、`ensures` 等规约关键字，以及数学整数类型 `int`、`nat` 等新类型。 证明一个 Rust 函数满足其后置条件（`ensures` 子句），或调用方满足函数的前置条件（`requires` 子句），往往颇具挑战。因此，本教程从简单概念（整数基本证明）起步，逐步过渡到中等难度（数据结构的归纳证明），再深入到高级主题（使用 `forall` 与 `exists` 的数组证明、并发代码证明等）。 所有证明均由自动定理证明器（具体为 [Z3](https://microsoft.github.io/z3guide/docs/logic/intro)，一款 SMT 求解器）辅助完成。 对于布尔或整数算术等简单性质，Z3 通常无需程序员额外干预即可自动证明；更复杂的证明则需要程序员与求解器协同。本指南将帮助你理解 SMT 求解器的能力与局限，并给出当求解器无法自动完成时如何补全证明的建议。（例如，SMT 通常无法自动完成归纳证明，但你可以通过编写递归 Rust 函数，并在其 `ensures` 子句中表达归纳假设，来手写归纳证明。） https://verus-lang.github.io/verus/guide/getting_started.html https://verus-lang.github.io/verus/guide/getting_started.html