形式化验证中最困难的部分从来不是验证器本身，而是编写证明。

给一位资深Rust工程师Verus——微软研究院开发的基于SMT的验证器——他可以在一个下午内为函数添加前置条件和后置条件注释。然后验证器会以机械确定性告诉他，该函数是否对所有可能的输入满足这些契约。这部分令人满意。

接着他遇到了循环。验证器抱怨无法建立后置条件。工程师需要一个不变量——一个在每次迭代前后都成立的逻辑陈述。寻找这个不变量过去需要博士学位，或者至少四十小时的反复试错。发表于OOPSLA 2025的AutoVerus利用LLM智能体网络将这项工作自动化了90%以上。中位数的证明任务在30秒内或三次LLM调用内解决。

以下是它的实际工作原理、成本以及仍然失效的地方。

真正的瓶颈是不变量搜索，而非SMT求解器

Verus通过幽灵代码、前置条件和后置条件扩展了Rust。你写的代码类似这样：

use vstd::prelude::*;

verus! {
    fn sum(arr: &[i32]) -> (result: i32)
        requires
            arr.len() <= 0x40000000,
        ensures
            result == spec_sum(arr@),
    {
        let mut total = 0;
        let mut i = 0;
        while i < arr.len()
            invariant
                0 <= i <= arr.len(),
                total == spec_sum(arr@.subrange(0, i as int)),
        {
            total = total + arr[i];
            i = i + 1;
        }
        total
    }
}

requires子句是前置条件。ensures子句是后置条件。while循环内的invariant块是让证明通过的关键。它告诉SMT求解器每次迭代中什么保持为真。

困难的部分是不变量。total == spec_sum(arr@.subrange(0, i as int))并不直观。人类通过归纳地思考处理前i个元素后什么保持为真来写出它。AutoVerus将不变量综合视为由验证器反馈引导的搜索问题，从而自动生成它。

AutoVerus如何将LLM智能体用作搜索策略

AutoVerus不是对GPT-4的单一提示。它是一个专业智能体的流水线，彼此传递结构化上下文。

第一个智能体读取你的Rust函数及其文档注释。它提取验证条件并生成requires、ensures和invariant子句的初始草案。

第二个智能体将这些注释输入Verus。Verus编译带注释的代码，并要求其SMT求解器（通常是Z3）消除证明义务。如果求解器回答UNSAT，则性质成立。如果回答SAT，则生成反例。大多数情况下，初稿会失败。

修复智能体读取验证器错误消息和失败的证明义务。它建议更强的不变量、更紧的界限或辅助引理。循环重复：生成、验证、修复。AutoVerus报告的中位数收敛为三次LLM调用。超过一半的150个非平凡基准任务在30秒内完成。

关键洞察不是LLM在逻辑上非常出色。证明搜索是一个局部优化问题，而LLM在猜测局部改进方面足够好，能比手工输入的人类更快地导航搜索空间。

90%这个数字实际意味着什么

AutoVerus在150个非平凡Rust证明任务基准上实现了超过90%的证明自动化。这些任务包括数组边界推理、循环累积和递归结构遍历。基准来自真实的Verus代码库。

90%的数字意味着LLM流水线生成了Verus无需人工干预即可接受的证明。这并不意味着规范是程序员预期的。LLM从函数名、文档注释和类型签名推断意图。如果你的函数名为process，文档注释写的是”handles the thing”，生成的规范将是通用的，可能是错误的。

这与Copilot为代码生成引入的分工相同。LLM写初稿，人类审查领域正确性。区别在于错误的证明是沉默的。通过验证的生成证明可能证明了错误的性质。你仍然需要理解函数应该做什么的人。

AutoVerus不能做什么

AutoVerus受限于Verus能表达的内容。Verus处理Rust的一个子集。它不支持异步、闭包或某些标准库集合。如果你的代码用tokio生成任务，AutoVerus目前还帮不了你。

AutoVerus也受限于模式。90%的成功率适用于看起来像训练分布的代码：数组上的循环、算术累积、边界检查。如果你的证明需要非显而易见辅助引理，修复智能体可能循环直到达到迭代限制。那时你就得手写证明了。

成本也不是零。基准任务每个证明花费几美分。一个完整模块可能花费十到三十美元的API调用。这比验证工程师的时间便宜两个数量级，但不是免费的。

在实际代码上运行AutoVerus

AutoVerus可从微软研究院获取。仓库是GitHub上的microsoft/verus-proof-synthesis。它要求你已安装Verus。

实际工作流程如下：

# 1. Install Verus
git clone https://github.com/verus-lang/verus.git
cd verus && source ./source/vstd.sh

# 2. Clone AutoVerus
git clone https://github.com/microsoft/verus-proof-synthesis.git
cd verus-proof-synthesis

# 3. Set your API key for the LLM backend
export OPENAI_API_KEY="sk-..."

# 4. Run AutoVerus on a Rust file
python autoverus.py --input src/my_module.rs --output src/my_module_verified.rs

输出是一个带requires、ensures和invariant子句注释的Rust文件。审查每个注释。然后运行Verus：

verus src/my_module_verified.rs

如果Verus报告verification results:: verified，则SMT求解器已消除所有义务。如果报告错误，将其反馈回AutoVerus进行另一轮修复，或手动修复。

对于CI集成，将Verus视为仅在带注释模块上运行的独立作业。Verus验证时间随注释复杂度增长。从你害怕的函数开始：解析器、协议状态机、任何索引到不受信任缓冲区的代码。

何时使用AutoVerus，何时放弃

当你有适合Verus子集的Rust代码且想要无界正确性证明时，AutoVerus值得尝试。Kani提供无需注释的有界证明，对崩溃自由检查更快，但无法证明跨越无界循环的性质。AutoVerus提供完整的无界证明，代价是需要它主要为你生成的注释。

如果你的代码是异步的、使用复杂闭包，或需要关于活性性质的证明（如”每个请求最终都会得到响应”），请放弃。对于活性，你仍然需要TLA+。如果你的证明需要自定义数学理论，请放弃。LLM智能体不会发明新数学。它们检索并适应以前见过的模式。

诚实的底线

AutoVerus并未消除理解代码的必要性。它消除了为你已经理解的代码花费四十小时编写不变量的必要性。转变是从证明工程到提示工程：你描述意图，智能体搜索证明空间，SMT求解器认证结果。

这一转变足以将形式化验证从专家小众领域转变为CI流水线步骤。对于应用程序与不受信任网络输入之间的三十行解析代码，现在可以实际证明它们不会恐慌。证明在几秒钟内生成，在几分钟内检查，由知道解析器应该做什么的人审查。

从一个函数开始。写Rust。运行AutoVerus。阅读注释。如果它们符合你的意图，你就有了一个机器检查的证明。如果不符合，你有一个比空白页更好的起点。

Frequently Asked Questions

What is AutoVerus and how does it relate to Verus?

AutoVerus is an automated proof generation system built on top of Verus, a Rust verifier from Microsoft Research. Verus checks whether annotated Rust code satisfies its specifications using an SMT solver. AutoVerus generates those annotations using a network of LLM agents.

How accurate is AutoVerus at generating proofs?

On its benchmark of 150 non-trivial Rust proof tasks, AutoVerus achieved over 90% automation. More than half resolved in under 30 seconds or three LLM calls. Accuracy depends on how closely your code matches the training distribution patterns.

Does AutoVerus eliminate the need to learn formal verification?

No. You still need to understand the annotations to review them for correctness. A generated proof that passes verification may prove the wrong property if the LLM misread your intent. AutoVerus reduces proof writing time from days to minutes, but it does not replace human judgment.

What Rust code works with AutoVerus?

Code that fits the Verus subset: functions with loops, array indexing, arithmetic, and recursive structures. AutoVerus does not support async, closures, or many standard library collections. It is best suited for systems code, parsers, and algorithmic functions.

How much does AutoVerus cost to run?

The benchmark tasks cost cents per proof. A full module might cost ten to thirty dollars in API calls. This is significantly less than the 40 to 80 hours of engineering time required for manual proof writing.