Claude 写出 1.8 亿行证明代码，抓出模糊测试多年未发现的漏洞
Claude 与 Theorem 合作，为编译后的 RISC-V 二进制文件生成了 1.8 亿行 Rocq 证明代码
Anthropic 于 10 月 22 日发布的研究 显示，Claude 与形式化方法初创公司 Theorem 合作，针对 239 个模糊测试入口点，对 123 个开源库完成了形式化验证，过程中生成了约 1.8 亿行经机器检查的证明代码。团队称，这是首次在编译后机器指令层面、用 AI 对生产级软件做大规模形式化验证；这些证明还找出了真实漏洞，而多年的自动化模糊测试在结构上根本无法发现它们。
这一区别之所以重要，源于形式化证明有一条硬性的逻辑限制：只要在给定空间内存在任何一个不安全的输入，就无法完成「该空间内所有输入都安全」的证明。也就是说，尝试验证这件事本身，就是一次系统性的反例搜索，而且覆盖了模糊测试永远不会到达的区域。
为什么模糊测试有结构性的天花板
谷歌的 OSS-Fuzz 项目自 2016 年起持续测试数百个开源库：向程序输入随机变异的数据，监测崩溃、内存损坏和 AddressSanitizer 违规，已发现数万个漏洞。但它测试不了自己从未生成过的输入。
OSS-Fuzz 通常把输入大小限制在 1 MB 左右。这并非随意之举：输入越大，模糊测试的吞吐量就越低，每秒能跑的测试用例也越少。对多数威胁模型而言这一取舍可以接受，但它留下了一个缺口。
在 Claude 受命验证的其中一个库里，解压缩器存在一个计数器下溢漏洞，只有输入约 20 MB 且布局极为特殊的数据时才会触发。标准规模的模糊测试永远不会生成这样的输入。证明尝试迫使 Claude 对最大 64 MB 的所有输入进行推理；当它试图证明整个空间都安全时，证明失败了，因为那个 20 MB 的反例确实存在。这个漏洞是验证尝试的逻辑结果，而不是靠随机碰运气撞出来的。
Anthropic 团队表示，这种方法目前已在受检的各个库中以这种方式发现了数百个漏洞。
由 Rocq 检查证明，Claude 不给自己打分
Claude 生成的证明用 Rocq 编写。Rocq 是 INRIA 开发的形式化证明助手，以归纳构造演算（Calculus of Inductive Constructions）为基础逻辑。Rocq 的内核会按严格的逻辑规则检查提交证明中的每一步推理。通过 Rocq 检查的证明，在该模型内数学上保证有效；系统不接受近似或概率性的论证。
这种架构对可信度很关键：证明由 Claude 生成，但验证者 Rocq 是独立开发的外部系统。AI 的输出不靠自己证明自己。
验证针对的是编译后的 RISC-V 机器码，而不是 C 或 C++ 源代码。这在技术上更难，因为证明必须考虑编译器施加的所有转换。Theorem 提供了让这一切成为可能的形式化语义：RISC-V 指令行为和 Linux 进程状态的数学模型，为 Rocq 推理二进制文件实际做了什么提供了精确的基础。
391 行 C 代码、63 万行证明，以及通向共享覆盖的路径
证明代码与源代码的比例说明了形式化验证在实践中的要求有多高。对 cJSON 库的单个入口点（391 行 C 代码），Claude 生成了约 63 万行 Rocq 证明。证明不仅要覆盖被检查的这 391 行，还要覆盖这些代码调用的每一个底层库函数。
为了应对这一工作量，Claude 编写了能自动生成一半以上证明内容的工具。证明还能复用：多个库调用相同的底层函数时，针对这些共享组件的证明可以直接沿用。在共享证明工作区的实验中，同样的验证任务少用了 17% 的 token，覆盖范围越大，节省越可观。在 36 项基准任务上，Claude Opus 5.5 完成工作所用的 token 比 Opus 5 少约 40%，让这种方法在算力成本高到无法承受之前能走得更远。
Anthropic 已公开发布 123 个库中 25 个库的证明，涵盖 60 个入口点，供开源项目维护者下载和复用。长期的可扩展性逻辑类似数学领域的 Mathlib：证明建立在共享、累积、经过验证的基础之上，每个进入公共库的新证明，都会降低验证下一个相邻组件的边际成本。
防御刻不容缓，而攻击方已经更快
这项研究的发布时机并非偶然。就在 Anthropic 发布的前一天，微软披露，被评估与中国国家利益一致的威胁行为者 Storm-0940，使用名为 ARTEX 的 AI 智能体框架自动化入侵行动，攻击了 2,250 多个租户。在多起得手的案例中，攻击者从初始访问到取得云级权限用时不到三小时。
同样在 10 月 21 日，PHP 项目发布了两个严重漏洞的补丁：CVE-2026-109618 和 CVE-2026-109619，CVSS 评分均为 9.2。它们由 Wiz Research、Calif 和 OpenAI 借助 Wiz Atlas、Gemini 4 Argon 和 GPT-5.6 Sol 做 AI 辅助分析发现。这些漏洞影响可追溯到 5.4 的 PHP 版本，意味着它们在无人察觉的情况下潜伏了十多年。大约 70% 的网络服务器运行 PHP。Cloudflare 首席执行官 Matthew Prince 表示，补丁公告发布后的数小时内，Cloudflare 网络上就观察到数百万次利用尝试。
PHP2Shell 事件清楚地说明了这种不对称：AI 已经在广泛部署的软件中找出了存在十年的缺陷，而攻击者在漏洞披露后数小时内就开始利用。
Anthropic 的网络安全使命（Cyber Mission）于 10 月 8 日启动，有 11 家创始合作伙伴，明确承认了这种态势。Anthropic 副首席信息安全官 Jason Clinton 呼吁安全负责人立即争取董事会层面对基线防御的支持，并估计未来约 18 个月形势会先恶化，之后才会好转。
这种方法尚未解决的问题
这种规模的形式化验证仍受到诸多重要限制。该技术目前需要 Theorem 为目标架构和运行环境构建的形式化语义模型，因此覆盖范围仅限于 RISC-V 上的 Linux 进程。扩展到其他平台需要新的模型，而构建它们绝非易事。
漏洞确认和修补仍然需要人工介入。对于电网、水处理系统、工业设备等关键基础设施，漏洞确认后部署修复在操作上很复杂，有时甚至不可行，这与消费级系统上的软件补丁不同。
所有公布的数据都是公司自报的：证明行数、token 节省估算、基准对比。证明有效性和所称效率提升的独立评估尚未发布，在这些结果影响全行业安全标准之前，这样的评估是必要的。
最大的悬而未决的问题是，证明复用的扩展速度，能否快到让每个库的成本随公共库增长而下降。如果可以，汇编级的 AI 辅助验证就可能成为高价值开源项目的标准 CI 工具；如果成本曲线没有拐点，这项技术对关键目标仍有吸引力，但对广泛的开源采用来说过于昂贵，只是一种有用的专项能力，而不是新安全体系的基础。