在 Rust 生态中，unsafe 代码始终是内存安全的潜在隐患。尽管 Rust 的所有权系统能够在编译期排除大量悬垂指针和数据竞争，但底层系统编程场景（如操作系统内核、自定义分配器、FFI 交互）仍需要额外的验证手段。Verus 作为微软研究院推出的形式化验证工具，正是为解决这一痛点而生 —— 它允许开发者用纯 Rust 语法编写规范与证明，并通过 SMT 求解器 Z3 静态验证代码是否满足这些规范，且不引入任何运行时检查。
验证范式：从类型安全到属性证明
传统静态分析工具（如 Clippy）只能检测模式化的代码缺陷，而形式化验证的核心区别在于：开发者显式声明代码必须满足的属性（specification），验证器证明这些属性对所有可能的执行路径永远成立。Verus 的设计哲学是将这一过程尽可能融入 Rust 开发体验 —— 规范和证明代码均使用 Rust 语法编写，无需学习单独的验证语言。
Verus 引入的最核心概念是三代码模式（Three Code Modes）。第一种是执行代码（exec），即普通的可运行 Rust 代码；第二种是规范代码（spec），用于描述函数的输入输出约束，只能引用数学类型（如整数 int 而非机器整型 i32）且不能包含副作用；第三种是证明代码（proof），用于编写人工介入的证明步骤，可使用 assert、assume、assert ... by 等构造。这三种模式在同一个 Rust 函数中通过属性标记共存，Verus 会在编译时将它们分离处理：exec 代码生成可执行二进制，spec 代码用于生成验证条件，proof 代码则指导 SMT 求解器完成证明。
前置条件与后置条件：requires 与 ensures
函数级规范通过 requires 和 ensures 关键字表达。前者声明调用者必须满足的前置条件，后者声明函数返回时必须满足的后置条件。例如，一个除法函数可写作：
fn divide(a: i32, b: i32) -> (result: i32)
requires b != 0
ensures result * b == a
这个规范声明了除数非零的前置条件，以及结果乘以除数等于被除数的后置条件。Verus 会自动推导这个函数的验证条件，确保任何满足 requires 的调用都必然产生满足 ensures 的返回值。值得注意的是，ensures 中可以使用 old() 函数引用调用前的状态，这对于修改了输入引用的函数尤为关键 —— 比如 fn push(vec: &mut Vec<T>, value: T) ensures vec.len() == old(vec.len()) + 1 明确表达了向量长度必然增加一。
循环不变量：invariant 关键字
对于包含循环的代码，SMT 求解器默认无法推断循环执行后的状态，此时需要显式声明循环不变量（loop invariant）。不变量是每次循环迭代开始时必须为真的命题，开发者通过 invariant 关键字提供：
fn sum(vec: &Vec<i32>) -> i32
ensures result >= 0
{
let mut i = 0;
let mut total = 0;
while i < vec.len()
invariant i >= 0 && i <= vec.len()
invariant total >= 0
{
total += vec[i];
i += 1;
}
total
}
这里第一个不变量确保索引始终在合法范围内，第二个不变量确保累计和始终非负。当循环终止时（条件 i < vec.len() 为假），结合不变量可推导出 i == vec.len() 和 total 的最终属性，进而满足函数的后置条件。循环不变量的选择是形式化验证中最需要技巧的部分 —— 太弱则无法推导出目标属性，太强则可能无法在循环入口处证明成立。
unsafe Rust 的内存安全证明
Verus 对 Rust 生态最具吸引力的特性，是其对 unsafe 代码的验证能力。在 Rust 中使用原始指针、跨 FFI 边界、或手动管理内存时，编译器无法保证安全性，而 Verus 提供了显式的证明义务（proof obligation）来填补这一空白。开发者可以使用 ghost 类型 和 tracked 类型 表达资源的所有权：ghost 类型仅在验证阶段存在，不影响运行时布局；tracked 类型则用于追踪必须在证明中手动传递的资源。
以原始指针的解引用为例，Verus 要求显式证明指针非空且对齐：
fn dereference(ptr: *const i32) -> i32
requires !ptr.is_null()
ensures result == *ptr
Verus 会将这个 requires 转化为对指针有效性的检查。对于更复杂的场景，如自定义内存分配器，开发者需要定义不变量来约束堆块的结构、已分配与空闲区域的分界等。这些不变量本质上是对内存布局的数学描述，一旦证明成立，即可确信该分配器在所有使用场景下都不会产生内存错误。
证明性能与工程实践
SMT 求解的复杂度决定了验证并非总是即时完成。Verus 官方文档建议关注以下工程参数：当函数包含量化（forall/exists）时，避免在量化域中使用大范围整数或复杂递归结构；循环不变量的表达式应尽可能简洁，复杂的逻辑建议拆分为多个不变量分别证明；使用 assert ... by(bit_vector) 或 assert ... by(nonlinear_arith) 显式指定求解策略，可显著加速特定领域的证明过程。验证失败时，Verus 会输出反例输入，开发者可据此调整不变量或 requires/ensures 的表述。
在实际项目中，Verus 已被用于验证 Rust 标准库的部分实现、操作系统内核（如 Asterinas）的核心数据结构、以及并发内存分配器的正确性。这些案例共同验证了一个趋势：在对安全性要求极高的系统中，形式化验证正在从学术研究走向工程实用。
参考资料