Claude 形式化验证实验：123 个开源库的证明，究竟覆盖了什么

让 AI 检查自己写的代码，读者往往会担心：如果它连检查报告也编得像模像样，谁来发现问题？Anthropic 与 Theorem 在 10 月 22 日公布的实验，给出了一条更可核查的路线——让 Claude 写证明，再交给 Rocq 的证明内核检查。

Anthropic 的研究说明称，团队为 123 个开源库的 239 个入口生成了形式化证明。研究也允许在证明过程中发现并修复问题；涉及代码修改时，结论必须对应修改后的二进制，不能套回旧版本。这项工作的看点，是把证明用到真实软件入口，并让检查结果不必依赖 Claude 自己的口头保证。要理解它到底进步了多少，得先读清楚“证明了什么”。

测试在寻找反例，证明在回答一个限定的问题

Google OSS-Fuzz 的说明介绍了模糊测试的思路：不断给程序喂入生成的数据，寻找能触发错误的输入。它已经是开源软件安全工作的重要组成部分。测试跑得越多，越可能碰到隐藏的路径；但“到现在还没碰到”仍然不能直接推出“所有输入都没问题”。

形式化验证把问题写成精确的命题，再给出能够被机器检查的推导。Rocq 官方介绍说明，它是一种证明助手，可用来描述程序规格，并证明程序符合这些规格。AI 可以反复尝试构造证明，最终是否成立由证明检查器按规则判断。

举一个帮助理解的假设例子：文件解析器接到某种数据就可能崩溃。模糊测试会尝试大量文件，争取找到触发条件；形式化证明则可能针对“所有满足输入和资源约束的文件，都不会让这个入口崩溃”建立推导。后者更有力的部分，在于覆盖命题范围内的所有情况；它的边界，也恰好在“满足哪些约束”这几个字里。

来源：Anthropic 原文图 2动画第 44 秒静帧，2026 年 10 月 24 日核查。绿色结论依赖蓝色组件正确；英文原图保留了这一条件。

123 个库，不等于 123 个库的所有代码都安全

入口可以理解为进入程序的一条门。从这里走得到的代码，与整个库里的全部功能，并不是同一个集合。实验所述“不崩溃”还带有条件，包括小于 64MB 的输入，以及采用单线程、静态链接的 RISC-V 程序。它不能原封不动地推广到日常服务器上任意架构、任意编译版本的同名软件。

另一个必须区分的数字来自 公开证明仓库：截至本文核查，README 列出的是 25 个库、60 个入口已有证明，不是研究报道中的全部 123 个库、239 个入口。研究总体结果与当前公开材料的范围不同，不能把前者写成后者已经全部可复核。

仓库还解释，证明针对具体编译出的二进制及既定命题，比较普通构建与启用错误检测的构建，论证规定范围内的行为一致，并排除检测器能够捕获的错误。这不等于程序的每个业务结果都正确，也不自动排除内存泄漏等检测器未覆盖的错误；当前这批公开证明也没有给出“程序一定会结束”的终止性保证。

这些限制具有实际含义。例如，解析器对所有覆盖的输入都不崩溃，仍然可能把某个字段解释错；程序持续运行，也可能让用户一直等不到答案。安全、功能正确和会在合理时间结束，是需要分别写进规格、分别论证的要求。

真正需要人盯住的，是证明前面的规格和假设

证明检查器可以拦住不符合规则的推导，却不能替人决定产品究竟应该做什么。若规格漏写了关键需求，证明通过也不能补上这个需求。把“返回正确金额”遗漏成“只要不崩溃就行”，得到的保证就会比用户需要的窄很多。

Theorem 的 Linux 进程语义模型说明也明确表示，模型并不完整，只描述部分 Linux 行为，并包含尚未检查的假设。因此，要把证明当成真实系统的安全证据，除了看 Rocq 是否通过，还要核对运行环境是否符合模型范围。这里的“独立检查”，指检查过程由另外的证明内核完成；本文并未独立重跑整个实验。

这也让它与通常的 AI 代码审查有了区别。模型建议“这里可能有越界”仍需要工程师追查；能提供完整命题、对应二进制和可检查证明，则给审查者多了一种具体证据。此前报道的 AI 智能体削弱安全监控事件，也提示我们应当检查智能体的实际行为，不能只采信它自己的结果描述。测试仍然有价值，它能帮助发现规格遗漏、环境差异和未纳入证明的功能，二者可以协作。

下一步的难题，是让这套方法承担日常工程成本

Theorem 在 9 月 29 日发布、10 月 19 日补充更新的路线分析提出，共享基础库的证明可以供依赖它们的软件复用，降低重复工作。其大规模验证时间表建立在能力持续提升等假设上，应当视为研究路线估算，不能当作已经完成的工程交付。

对软件团队，这次实验最值得观察的后续，是覆盖范围能否逐步扩大、公开材料能否支持外部复核，以及代码更新后证明能否低成本跟着更新。源码修复一次，编译产物就可能改变，旧证明对应的对象也需要重新核对。

因此，评估这类工具时，交付物不能只是一份写着“验证通过”的报告。规格、软件版本、环境假设和证明应当能够对应起来；更新之后，也应该说明哪些保证依然成立。这些细节做好了，形式化验证才有机会进入开发团队的日常工作。

本文依据研究说明与公开项目文档撰写，资料核查截至 2026 年 10 月 24 日。