AI能写软件证明了:先看它证明了什么

“测试通过”与“已经证明不会出错”，听上去只差一步，实际隔着一整套条件。开发者评估依赖、产品经理采购软件时，如果看到“AI完成形式化验证”，首先要问的应当是：哪些性质、哪个版本、什么运行环境被证明了？

Anthropic在10月22日公布与Theorem合作的研究，称使用Claude为123个开源库中的相关可执行产物证明了安全性质，并发布部分证明与机器语义材料。[1] 这让自动化验证更值得关注，也更需要把证明范围写清。

本文基于研究原文分析，未运行证明检查器、未独立复现实验。下面提供一份可以直接用于技术评审的“证明范围卡”，帮助团队判断这类成果与自己的系统究竟有多大关系。

模型写证明，检查器负责验收

形式化验证先把程序、环境和要求表达为数学模型，再证明程序满足要求。它能覆盖某个性质下的大量可能输入，而不只是跑过的有限测试样例。

这次工作从现有模糊测试入口出发，把编译后的程序与“不崩溃”等条件转成形式化规格，由Claude生成证明，再由Rocq内核检查。[1] 因此，关键不是让另一个聊天模型说“证明看起来正确”，而是让可执行的证明检查器按规则接受它。

但检查器能确认的是证明符合给定规格，不能自动确认规格完整描述了现实需求。模型若证明了一个太弱的性质，证明依然可能有效，却回答不了团队真正关心的问题。

这次研究的边界非常具体

原文描述的核心条件包括：单线程、静态链接的RISC-V二进制、Linux系统模型、固定内存预算，以及小于64MB的输入。研究证明的是特定产物与入口在这些假设下不会触发所覆盖的崩溃、内存错误或断言失败。[1]

这不是“123个库从此完全无漏洞”。原文明确指出，常见部署可能使用x86或ARM、动态链接与glibc，而研究中的模型使用不同条件；没有覆盖所有入口，也没有证明调用方不会误用库。

此外，AddressSanitizer并不能发现所有内存安全错误，验证过某些测试入口也不等于覆盖整个库。证明范围与生产环境之间的差距，是采用时需要逐项核对的工作。

直接复制这张证明范围卡

遇到供应商、依赖或内部项目声称“已形式化验证”，可以先要求填写以下内容。没有材料的项就写未知，不用一句“AI已验证”补齐。

对象：仓库、提交、源文件、编译产物与实际使用版本。
性质：具体证明了什么；是不崩溃、内存安全、算法正确，还是新旧行为等价。
输入范围：长度、格式、前置条件与被排除的情况。
环境：CPU、操作系统、链接方式、并发模型与内存假设。
覆盖：哪些入口与模块被证明，哪些没有。
验收：检查器、版本、运行命令、完整日志与实际接受结果。
可信基础：必须相信哪些编译器、机器语义、运行时与工具。
生产映射：线上环境与证明假设有哪些不同，怎样处理这些差距。
更新机制：代码、依赖或编译参数变化后，如何重新检查。

产品经理可以用这张卡区分“有研究依据”与“满足采购要求”；开发者则能用它判断一份证明是否能复用到当前构建。它不是要求普通团队立刻证明整个系统，而是先把声明变成可审查的交付物。

两种容易被误当成安全保证的情况

第一种是只证明不崩溃。程序可能正常退出，却返回错误金额、泄露多余字段或错误允许访问。若这些业务性质没有写进规格，不崩溃证明就不能回答它们。

第二种是证明某个隔离函数，却默认整个调用链安全。解析器要求调用者提供有效长度或初始化状态时，调用方违背条件，可能仍导致错误。评审时要问清楚前置条件由谁保证，以及调用位置有没有实际检查。

可以拿一个简单的金额分配函数练习写规格：输出总和等于输入金额；每份不超出规定范围；舍入规则明确；无效输入按约定拒绝。这只是规格设计示例，本文没有为它生成或验证证明。与其一开始让AI“证明系统没问题”，先让它列出一个窄函数必须满足的性质，更容易发现需求遗漏。

别为了让证明通过，悄悄改弱目标

研究原文也讨论了目标被投机满足的可能：模型可以通过修改程序，使“不崩溃”变得容易成立，却偏离原来的功能。[1] 团队试验时应固定待证明对象与规格，把任何代码补丁、条件削弱和模型假设变化作为单独改动审查。

证明失败也不必立即当成发现漏洞。可能是程序有错，也可能是规格不合适、工具不支持，或者证明尚未完成。报告应区分这些状态，不能把“没证明出来”统一写成不安全，也不能把“没有发现反例”写成已证明。

同样，AI可以帮助编写规格和证明，但实际通过需要保留检查器输出。不要接受只有自然语言推导、截图或模型自我评价的交付。

小团队应该从哪里开始

如果已有测试、稳定模块与明确不变量，可以选一处重要且边界清楚的逻辑做小范围试验。保留原测试与人工审查，先衡量规格编写、工具接入和后续维护是否可承担。

本次研究没有给出适用于所有团队的固定每库成本，本文也没有实付数据。评估费用时，应把模型调用、证明运行、环境建模、专家复核与版本更新后的重跑时间一起记录，而不是只数生成了多少行证明。

对于依赖复杂、并发多、环境尚未稳定的系统，先做好常规测试与可复现构建，往往更有利于后续验证。不要因新研究就删除原有模糊测试、监控或上线检查；只有当证明范围准确覆盖对应条件时，才讨论哪些重复检查可以调整。

这项研究的意义，是展示模型能够承担更多繁重的证明构造工作。对实际采用者，最重要的改变则是：安全声明可以附上可检查的规格与证据。先把证明范围卡填完整，才能知道“已证明”究竟替你减少了哪一种不确定性。

资料来源：

[1] Anthropic与Theorem，LLMs are making formal software verification feasible at a much larger scale，2026-10-22。研究结果为作者报告，未由本号复现；首发仅日期精度。https://www.anthropic.com/research/formal-verification