Verus：基于 Rust 验证代码正确性，指南助你掌握验证概念与技术！

键盘快捷键

按 `←` 或 `→` 可在各章节间导航；按 `S` 或 `/` 能在本书中搜索；按 `?` 可显示此帮助信息；按 `Esc` 则可隐藏此帮助信息。

模式选项包括：

• 自动
• 明亮模式
• Rust 模式
• 煤炭模式
• 海军蓝模式
• Ayu 模式

Verus 教程与参考手册

Verus 概述

Verus 是用于验证用 Rust 编写的代码正确性的工具。其主要目标是基于现有验证框架（如 Dafny、Boogie、F*、VCC、Prusti、Creusot、Aeneas、Cogent、Rocq 和 Isabelle/HOL）的理念，验证底层系统代码的完整功能正确性。验证是静态的，Verus 不会添加运行时检查，而是使用计算机辅助定理证明来静态验证可执行的 Rust 代码在所有可能的执行情况下都能满足用户提供的某些规范。

更详细地说，Verus 的目标如下：

• 提供一种纯数学语言来表达规范（类似于 Dafny、Creusot、F*、Coq、Isabelle/HOL）。
• 提供一种基于经典逻辑（类似于 Dafny）的数学语言来表达证明（类似于 Dafny、F*、Coq、Isabelle/HOL）。
• 提供一种基于 Rust（类似于 Prusti、Creusot 和 Aeneas）的底层命令式语言来表达可执行代码（类似于 VCC）。
• 基于以下原则生成小型、简单的验证条件，以便像 Z3 这样的 SMT 求解器能够高效求解：
• • 使数学规范语言与 SMT 求解器的数学语言相近（类似于 Boogie）。
  • 使用轻量级线性类型检查而非 SMT 求解来推理内存和别名问题（类似于 Cogent、Creusot、Aeneas 和 线性 Dafny）。

我们认为 Rust 是实现这些目标的理想语言。Rust 将底层数据操作（包括手动内存管理）与先进的高级安全类型系统相结合。该类型系统包含了高级验证语言中常见的特性，如代数数据类型（支持模式匹配）、类型类和一等函数。这使得以自然的方式表达规范和证明变得容易。更重要的是，Rust 的类型系统对线性类型和借用提供了复杂的支持，这处理了大部分关于内存和别名的推理。因此，剩余的推理可以忽略大多数内存和别名问题，将 Rust 代码视为纯函数式语言编写的代码，从而使验证更加容易。

目前，我们不打算：

• 支持所有 Rust 特性和库（相反，我们将专注于支持用户所需的高价值特性和库）。
• 验证验证器本身。
• 验证 Rust/LLVM 编译器。

本指南

本指南假设你已经对 Rust 编程的基础知识有一定了解。（如果你还不了解，我们建议你花几个小时浏览 学习 Rust 页面。）熟悉 Rust 对使用 Verus 很有帮助，因为 Verus 基于 Rust 的语法和类型系统来表达规范、证明和可执行代码。实际上，并没有单独的规范和证明语言；规范和证明都是用 Rust 语法编写，并使用 Rust 的类型检查器进行类型检查。因此，如果你已经掌握了 Rust，那么开始使用 Verus 会更容易。

然而，验证 Rust 代码的正确性需要一些超出编写普通可执行 Rust 代码的概念和技术。例如，Verus 通过宏扩展了 Rust 的语法，引入了用于编写规范和证明的新概念，如 `forall`、`exists`、`requires` 和 `ensures`，还引入了新的类型，如数学整数类型 `int` 和 `nat`。证明一个 Rust 函数满足其后置条件（`ensures` 子句）或一个函数调用满足其前置条件（`requires` 子句）可能具有挑战性。因此，本指南的教程将带你逐步了解各种概念和技术，从相对简单的概念（关于整数的基本证明）开始，过渡到中等难度的挑战（关于数据结构的归纳证明），然后再到更高级的主题，如使用 `forall` 和 `exists` 对数组进行证明以及对并发代码进行证明。

所有这些证明都借助了自动定理证明器（具体来说是 Z3，一个可满足性模理论求解器，简称 “SMT 求解器”）。SMT 求解器通常能够在无需程序员额外帮助的情况下证明简单的属性，如布尔值或整数算术的基本属性。然而，更复杂的证明通常需要程序员和 SMT 求解器共同努力。因此，本指南还将帮助你了解 SMT 求解的优势和局限性，并提供如何填补 SMT 求解器无法自动处理的证明部分的建议。（例如，SMT 求解器通常无法自动进行归纳证明，但你可以通过编写一个递归的 Rust 函数，其 `ensures` 子句表达归纳假设，来编写归纳证明。）