你想对代码做形式化验证，却不知道从哪里开始

你想对代码做形式化验证，却不知道从哪里开始。 第 1 课：你的第一个经过验证的 Rust 二进制程序。 现在就能对部分 Rust 代码进行可证明的验证，无需更换语言，就能移除整类测试。我用 Verus 演示一个简短例子。 步骤 0：安装 Verus（链接在回复里）。 步骤 1：在现有仓库中执行： cargo add vstd 然后在 Cargo.toml 添加两行： [package.metadata.verus] verify = true 如果从零开始，cargo verus new --bin clamp 会替你完成这些。 步骤 2：用 verus! 包住函数，并写出它必须满足的规格。 这里是 clamp。它把数字限制在一个范围内：clamp(150, 0, 100) 返回 100。规格要求结果始终落在范围内，原本就在范围内的数字则原样返回。 use vstd::prelude::*; verus! { fn clamp(x: i64, lo: i64, hi: i64) -> (r: i64)     requires       lo <= hi,     ensures       lo <= r <= hi,       lo <= x <= hi ==> r == x,   {     if x < lo { lo } else if x > hi { hi } else { x }   } } // verus! fn main() {   println!("{}", clamp(150, 0, 100)); } Verus 就放在仓库现有的 Rust 源文件中。如上所示，规格写在它描述的代码正上方。Verus 检查 verus! 内部内容，忽略其余部分，所以可以逐个函数启用。普通的 cargo build 仍然有效。Verus 支持 Rust 的一个子集，因此先从小型、独立的函数开始。 这最终能替代 Agent 针对不同场景和边界情况写出的全部 clamp 测试。测试只能检查包含在测试里的输入，而这份证明检查了每一种可能的输入，验证了代码正确性。 像结对编程一样，与编码 Agent“结对验证”。一起写规格，然后让 Agent 向你解释每条 requires 和 ensures，让你明白正在证明什么，也确保 Agent 理解你的意思。确认 Agent 理解你表达的含义，就是理解你的意图。这一点至关重要，否则可能写出毫无意义的形式化规格和证明，让代码库膨胀。 满意之后，再让编码 Agent 证明它： cargo verus verify → 1 verified, 0 errors 交付：执行 cargo verus build，运行二进制程序，得到 100。规格在编译时被移除。 就这样。代码经过验证，代码库和 CI 也少了一堆冗余测试。