不写一行证明也能证明 Rust 代码正确。干这活的工具叫做模型检验器，目前对 Rust 最实用的一个是 AWS 开发的 Kani。你写普通的 Rust 断言，Kani 把它们转成数学命题，对所有可能的输入进行检验。不需要定理证明器，不需要证明辅助工具，也不需要一头扎进 Coq 半年出不来。

问题在于，“所有可能的输入”只有在输入空间足够小、可以穷举的时候才成立。如果你的函数接收一个有百万个元素的 Vec<u8>，Kani 不会检查每一种排列。它只会检查到你指定的边界为止，或者跑到你的笔记本内存耗尽。证明是真的，但它是有界的。

“无证明的证明”到底是什么意思

形式化验证通常意味着在 Coq 这样的证明辅助工具里写程序，手工定义不变式，用战术步骤引导求解器。像 CompCert 这样的验证编译器花了好几年。大多数团队没有好几年。

模型检验不一样。你写普通的 Rust。添加一个带有 #[kani::proof] 注解的验证函数。在里面用 kani::any() 生成符号值，调用你的代码，然后做出断言。Kani 把你的代码编译成逻辑公式，交给 SMT 求解器。求解器要么确认该性质在边界内的所有输入上都成立，要么给出一个具体的反例。

你没写证明。你写了一个带全称量词的测试。证明是工具写的。

Kani 如何把 Rust 变成逻辑

Kani 是一个有界模型检验器。它把你的代码展开成逻辑公式，问 SMT 求解器：有没有哪条执行路径会违反断言？求解器把变量当成符号处理。普通测试给 x 赋值为 5，Kani 的证明给 x 一个符号，代表所有可能的 u32。

下面是一个 trivial 的例子。我们有一个不应该溢出的函数，想证明这一点。

// src/lib.rs
pub fn saturating_double(x: u32) -> u32 {
    x.saturating_mul(2)
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    fn check_saturating_double_never_overflows() {
        let x: u32 = kani::any();
        let result = saturating_double(x);
        if x > u32::MAX / 2 {
            assert_eq!(result, u32::MAX);
        } else {
            assert_eq!(result, x * 2);
        }
    }
}

运行 cargo kani，Kani 在数秒内完成验证。它不逐个执行，就检查了 x 的全部 4,294,967,296 种可能取值。SMT 求解器从符号表示出发进行推理，得出结论：不存在反例。

#[cfg(kani)] 守卫意味着这段代码只在 Kani 下编译，不会膨胀你的发布版本。

真实例子：证明一个解析器永不崩溃

溢出是简单的情况。有意思的案例是数据相关的。假设我们有一个解析小型协议头的函数，想证明无论喂给它什么字节，它都绝不会 panic。

// src/protocol.rs
#[derive(Debug, PartialEq)]
pub enum ParseError {
    TooShort,
    InvalidVersion,
}

pub struct Header {
    pub version: u8,
    pub length: u16,
}

/// Parse a 4-byte header:
/// - byte 0: version (must be 1)
/// - byte 1: reserved (ignored)
/// - bytes 2-3: length in big-endian
pub fn parse_header(buf: &[u8]) -> Result<Header, ParseError> {
    if buf.len() < 4 {
        return Err(ParseError::TooShort);
    }
    let version = buf[0];
    if version != 1 {
        return Err(ParseError::InvalidVersion);
    }
    let length = u16::from_be_bytes([buf[2], buf[3]]);
    Ok(Header { version, length })
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    #[kani::unwind(5)]
    fn check_parse_header_no_panic() {
        let len: usize = kani::any();
        kani::assume(len <= 8);
        let buf: [u8; 8] = kani::any();
        let _ = parse_header(&buf[..len]);
    }
}

Kani 验证 parse_header 对长度从 0 到 8 的所有输入缓冲区都不会 panic。它检查了边界测试、版本检查和数组索引。如果我们没有先检查长度就写了 buf[1]，Kani 会找到一个反例：一个 1 字节的缓冲区，buf[1] 越界。

#[kani::unwind(5)] 注解告诉 Kani 把循环展开多少次。由于我们的函数里没有循环，这个值是保守的。

边界化问题：模型检验撞墙的地方

模型检验在边界内是穷尽的。超出边界，它一言不发。这是根本的权衡。

循环是第一堵墙。Kani 必须把每个循环固定展开若干次。如果你的函数遍历一个 Vec，你把展开边界设为 10，Kani 证明长度为 0 到 10 的向量的正确性。它对长度 11 无话可说。每增加 1，状态空间就翻倍。展开 50 也许几分钟能跑完，展开 500 可能永远跑不完。

递归类似。每次调用都会膨胀公式。深度递归会让内存使用量爆炸。

数据大小是第二堵墙。Kani 擅长处理固定大小的数组。动态分配的集合除非显式限制大小，否则它很吃力。

标准库是第三堵墙。Kani 建模了其中很大一部分，但不是全部。如果你调用了 Kani 不理解的东西，证明会因为缺少函数定义而失败。

Kani 能证明什么、短板在哪里

Kani 擅长在有界代码中发现 panic、整数溢出和断言违反。它对密码学原语、协议解析器和小型状态机特别出色。这些地方的特点是：一个坏输入就能酿成灾难，而且代码天然有界。

Kani 不擅长证明活性性质，比如”每个请求最终都会得到响应”。这需要对无限执行进行推理，而有界模型检验明确不做这件事。对于活性，你需要像 TLA+ 这样的时序模型检验器。

Kani 也不能替代测试。通过证明意味着边界内不存在反例。通过测试意味着代码在你关心的某个具体输入上行为正确。Kani 抓住你想不到的边界情况。测试抓住 Kani 看不见的集成问题。

在 CI 里跑 Kani，别把 runner 跑崩

一个针对小函数的 Kani 证明只需数秒。一个真实 crate 的完整套件需要数分钟。展开边界高的证明可能跑上数小时。你不会想让 CI 管道等一个两小时的 SMT 求解。

保持 Kani 证明小而快。去证明安全攸关的函数——那些出了 bug 就是事故的函数。别试图证明你的整个 Web 框架。设置超时，比如每个证明 5 分钟，并且把超时视为”未能证明”，而不是”证明失败”。

以下是一个有效的 Makefile 模式：

# Makefile
kani:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 300 --all-functions --enable-unstable

kani-fast:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 60 --all-functions --enable-unstable

kani-fast 在每个 pull request 时跑 CI。kani 每晚跑。如果证明出现退化，你一天内就能发现，而不是在发货之后。

如果你暴露了公共 API，为每个公共函数写一个 Kani 证明，用完全符号化的输入去调用它。这是最接近形式化契约测试的东西。它不证明实现正确，但证明实现在任意有效输入上都不会崩溃。

什么时候该换真正的证明辅助工具

如果你需要证明关于无界数据结构的性质，比如”这条链表永远无环”，Kani 帮不了你。展开边界会推翻这个论断。这时候你需要 Creusot 这样的工具，它把 Rust 翻译成 WhyML，再用证明辅助工具。工作量更大，但能处理无界结构。

如果你需要等价性证明或未定义行为检测，MIRI 或 KLEE 这样的工具位于工作量与覆盖率的谱系上不同位置。Kani 是”我有有界代码，想知道它会不会 panic”的甜蜜点。解析器、解码器、序列化器和配置验证器都适用。Rust 的类型系统已经消灭了整个类别的 bug。Kani 消灭的是类型系统够不到的那些。

先尝试什么

如果你有一个 Rust crate，里面有个让你心里发毛的函数，加上 Kani。让你发毛的通常是解析不可信输入、做位运算、或者对数组做索引的函数。写一个证明框架，用 kani::any() 调用它。运行 cargo kani。通过了，你就得到了一个有界的崩溃自由证明；失败了，你就得到了一个具体的反例——那本来会是一个 bug 报告。

你不需要学一门新语言。你不需要理解序贯演算。你写 Rust 断言，求解器告诉你它们是否成立。这不是学术意义上的形式化证明，而是实用意义上的机械证明。而对大多数软件来说，实用恰恰就是你需要的。

常见问题

软件验证中的模型检验是什么

模型检验是一种自动化技术，它穷举系统的所有可能状态，以验证指定性质是否成立。对于 Rust，Kani 这样的工具使用有界模型检验来证明在限定边界内所有可能输入上的断言，无需手工构造证明。

Kani 与写单元测试有什么不同

单元测试检查一个具体输入。Kani 的证明检查边界内的每一个输入。如果 Kani 的证明通过，你就知道有界状态空间内不存在反例。证明更强，但受你设置的边界限制。

Kani 能证明我的整个 Rust 应用都正确吗

不能。Kani 最适合小型、有界的函数。状态空间随循环迭代次数、递归深度和数据大小指数增长。把 Kani 用在解析器、协议处理器这类安全攸关的组件上，而不是应用层逻辑。

当 Kani 遇到没有固定边界的循环时会发生什么

Kani 需要为循环指定展开边界。如果循环可能执行的次数超过边界允许，Kani 会插入一个失败的展开断言。你必须提高边界，或者重构代码使其具有静态已知的迭代次数。这是有界模型检验的主要限制。