Rust 形式化验证实战：基于 Kani 与 Prusti 的程序正确性证明

引言

系统级软件的可靠性一直是软件工程的核心挑战。Rust 语言虽然通过所有权系统和借用检查器在编译期消除了内存安全问题，但对于业务逻辑的正确性（如算法边界条件、并发不变量、协议一致性）则无能为力。形式化验证（Formal Verification）正是为此而生——它通过数学方法证明程序满足规约，从根本上消除一类 bug。本文深入探讨当前 Rust 生态中最具前景的两款形式化验证工具：亚马逊 Kani 和 Prusti，并通过真实工程案例展示它们如何落地到生产代码中。

1. 形式化验证基础概念

1.1 霍尔逻辑与弱前置条件

霍尔三元组 {P} C {Q} 表示：若前置条件 P 在执行语句 C 之前成立，则 Q 在 C 执行后成立。弱最前置条件（Weakest Precondition, WP）方法是形式化验证的核心理论工具：给定后置条件 Q 和代码 C，计算满足"执行 C 后 Q 必然成立"的最弱前置条件 wp(C, Q)。验证器的目标是证明用户提供的规约 P 蕴含 wp(C, Q)。

1.2 符号执行 vs 模型检测

形式化验证的两大主流技术路线：

• 符号执行（Symbolic Execution）：以符号值代替具体输入，探索程序的所有可能路径，对每条路径生成约束条件并传递给 SMT 求解器（如 Z3、CVC5）判定可满足性。Kani 采用此方法。
• 定理证明（Deductive Verification）：将程序规约转化为逻辑公式，通过最弱前置条件演算生成验证条件（Verification Condition, VC），再调用 SMT 求解器自动证明或交互证明。Prusti 采用此方法。

2. Kani 模型检查器

2.1 架构与设计哲学

Kani 是 AWS Labs 开发的 Rust 模型检查器（Model Checker），它将 Rust MIR（中级中间表示）转换为 GOTO-C 符号执行模型，再利用 CBMC（C Bounds Checker）作为后端求解引擎。Kani 的核心优势是完全自动化——用户只需添加 `#[kani::proof]` 标注和 `kani::assert()` / `kani::assume()` 即可启动验证，无需手写規约。

2.2 安装与配置

# 安装 Kani（需要 cargo 和 Rust toolchain）
cargo install --locked cargo-kani
cargo kani setup  # 下载预编译的 CBMC 求解器

# 在 Cargo.toml 添加依赖
[dev-dependencies]
kani = "0.0.0"

2.3 实战案例：排序函数验证

use kani;

#[kani::proof]
fn verify_bubble_sort() {
    let n: usize = kani::any_where(|&x| x <= 64);
    let mut arr: Vec = (0..n).map(|_| kani::any()).collect();

    bubble_sort(&mut arr);

    // 后置条件1：排序后长度不变
    kani::assert(arr.len() == n, "Length preserved");
    // 后置条件2：排序后数组单调非递减
    for i in 1..arr.len() {
        kani::assert(arr[i-1] <= arr[i], "Sorted order");
    }
    // 后置条件3：输出是输入的排列（通过元素计数验证）
    let mut sorted = arr.clone();
    sorted.dedup();
    kani::assert(sorted.len() <= n, "Elements preserved");
}

fn bubble_sort(arr: &mut [i32]) {
    let n = arr.len();
    for i in 0..n {
        for j in 0..n - i - 1 {
            if arr[j] > arr[j + 1] {
                arr.swap(j, j + 1);
            }
        }
    }
}

2.4 并发验证：Arc + Mutex 不变量检查

Kani 强大的并发验证能力允许开发者验证多线程代码中的数据竞争自由性和不变量保持。通过将 Mutex 保护的数据设为符号值，Kani 可以枚举所有可能的交织调度（Interleaving），证明无论线程执行顺序如何，共享不变量始终成立。

#[kani::proof]
#[kani::unwind(3)]  // 限制展开深度
fn verify_concurrent_counter() {
    use std::sync::{Arc, Mutex};
    use std::thread;

    let counter = Arc::new(Mutex::new(0));
    let c1 = counter.clone();
    let c2 = counter.clone();

    let h1 = thread::spawn(move || {
        let mut data = c1.lock().unwrap();
        *data += kani::any_where(|&x: &i32| x >= 0);
    });

    let h2 = thread::spawn(move || {
        let mut data = c2.lock().unwrap();
        *data += kani::any_where(|&x: &i32| x >= 0);
    });

    h1.join().unwrap();
    h2.join().unwrap();

    // 验证：最终值 = 两次增量之和（无数据竞争）
    let val = *counter.lock().unwrap();
    kani::assert(val >= 0, "Counter invariant held");
}

3. Prusti 验证工具

3.1 基于 Viper/硅验证引擎

Prusti 是瑞士苏黎世联邦理工学院开发的 Rust 验证工具，核心亮点是基于分离逻辑（Separation Logic）和 Viper 验证引擎，支持对堆内存操作和并发ownedship变动的精细规约。Prusti 使用 Rust 函数内的标注语法（如 `requires`、`ensures`）来表达前后条件，且支持幽灵变量（Ghost Variable）来引用函数调用前的值。

3.2 实凭案例：二叉搜索树插入规约

#[requires(true)]
#[ensures(result.contains(val))]
#[ensures(forall(|x: &i32|
    old(tree).contains(x) == result.contains(x)))]
fn bst_insert(tree: &mut BST, val: i32) -> BST {
    // 插入逻辑...
}

3.3 幽灵变量与 pledges

Prusti 引入的 pledge 标注允许指定在调用返回后某条件在某个future时间点被满足，这对验证带有延迟release的资源非常有価値。幽灵变量用于保存函数入口处的值（如 `old(tree).height`），在后置条件中引用以比较状态变化。

4. 生产级工程实践

4.1 逐步验证策略

在已有项目中引入形式化验证的策略：

1. 优先验证核心算法：排序、加密、共识协议等逻辑密集型模块
2. 聚焦边界条件：空集、最大值/最小值、溢出场景、并发死锁
3. 建立规约庫：将常见数据结构的行为规约抽象为可复用标注
4. CI集成：在 GitHub Actions 中运行 cargo kani 检查，设定 unwind 上限

4.2 局限与应对

• 状态爆炸：限制循环展开深度（`#[kani::unwind(N)]`），使用循环不变量阻断
• SMT求解器不完全性：浮点、非线性整数算术的不可判定性，使用整数逼近或区间算术替代
• 学习曲线：团队需要理解 SMT 反例报告，建议先从最简单的 GDB风格断言习惯培养起

5. 前沿展望

Rust 形式化验证生态正在快速演进：creusot 在探索基于 Why3 的验证路径，verus（原 Verus 系统）提供了类似 Dafny 的 Rust 验证语法。未来的趋势是降低使用门槛——IDE 集成实时规约检查、AI 辅助规约生成（LLM 提示函数意图并自动合成前后条件），以及从标准库开始构建默认verified规范。随着汽车功能安全（ISO 26262）和航空（DO-178C）对形式化方法需求的增长， Rust 验证工具将进入更多关键任务系统。