Anthropic与形式验证公司Theorem合作，称Claude在数周内为123个开源库的239个模糊测试入口生成了针对RISC-V二进制的形式化安全证明并修补发现的缺陷。研究展示了AI辅助生成可由Rocq检查器验证的证明流程及其在范围、平台和可复用性上的限制。
Anthropic于2026年10月22日公布与形式验证公司Theorem合作的研究：研究方称，Claude在数周内修补所发现的缺陷，并为123个开源软件库的239个模糊测试入口生成安全性质证明。证明针对编译后的RISC-V二进制程序，合计约1.8亿行Rocq代码。
这项研究试图改变软件安全的一种基本工作方式：不只是不断寻找能让程序出错的输入，而是在明确限定的运行环境和输入范围内，证明某类错误不会发生。但它并不意味着123个库已经没有漏洞，也不意味着常见服务器上的同名软件已获得同样保证。
从反复试错，转向证明特定错误不可能发生
模糊测试会向程序不断输入随机生成或变异的数据，寻找崩溃、断言失败等异常。它能发现大量缺陷，却无法仅凭运行时间足够长，就证明所有路径都已检查完毕。
Anthropic与Theorem的做法，是把开源项目已有的模糊测试转成形式化规格：对于规定范围内的任意输入，这个测试程序都不应触发指定错误。Claude随后围绕编译后的机器指令构造数学证明，由Rocq证明检查器核验。
如果生成证明的过程中发现反例，模型先修改代码，再针对修改后的程序重新生成规格和证明。因此，最终得到保证的对象可能是修补后的特定构建，不能据此推断上游项目原有版本天然安全。
研究方报告，这批证明覆盖123个OSS-Fuzz软件库的239个入口，典型证明约60万行，对应二进制程序的指令数中位数约为1.8万条。这些规模数字来自研究团队披露，并不是外部复现实验的结果。
证明代码很长，本身并非安全程度的衡量标准。关键在于所证明的命题是否有用、证明是否通过检查，以及命题和机器模型是否准确描述了现实系统。
不崩溃，也可能意味着更高层性质成立
测试入口不只检查内存访问。开发者也会把功能要求写成断言：例如先压缩再解压，结果应与原始输入一致；若不一致，测试便失败。
在这种情况下，证明所有受覆盖输入都不会触发失败，也就间接证明了断言所表达的功能性质。Anthropic以LZO压缩算法的往返测试为例，解释为什么不崩溃证明可以超出单纯的内存安全检查。
尝试证明的过程也可能找到模糊测试不容易撞见的缺陷。研究团队称，其中一个解压程序的问题需要约20 MB、布局特殊的输入才会触发；另有图像解码问题需要很大的输入和内存占用。这些案例说明，形式化推理可能触及由输入结构、长度或调用顺序共同决定的边界条件。不过，发现缺陷、完成修补和证明最终程序是不同环节，不能用其中一个环节替代另外两个。
证明的边界，比没有漏洞的口号更重要
这批主实验针对单线程、静态链接musl libc的RISC-V Linux程序，并设定输入和内存预算。Anthropic将输入上限表述为64 MB；Theorem的项目介绍则使用64 MiB。具体复查仍应以各二进制对应的形式化命题为准，而不是把介绍页的单位表述当成完整规格。
现实中，许多用户运行的是x86或ARM构建，采用动态链接，并依赖glibc。不同指令集、系统行为和链接方式都可能改变适用范围，RISC-V构建的证明不能直接迁移成这些部署的安全认证。
覆盖入口也不等于覆盖整个库。团队没有验证每个库的全部入口；即使所有测试入口都得到验证，未被入口触及的代码，以及调用方对接口的错误使用，仍可能留下风险。AddressSanitizer等检测工具也不能识别所有内存错误，更不自动排除错误计算结果等功能缺陷。
此外，证明检查器能判断形式化推导是否成立，却不能自行保证规格与真实机器完全一致。CPU、Linux进程和系统调用的模型，以及证明所依赖的工具和公理，仍是必须审视的信任基础。
公开的是一部分证明，而且不保证程序终止
Theorem的公开证明仓库目前列出25个库、60个入口的证明，涉及OpenSSL、simdjson、zstd等项目。这个公开子集不能与公告中的123个库、239个入口混为一谈。Anthropic也表示，不会公开可能暴露尚未修补漏洞的证明。
仓库README进一步解释了公开命题的含义：在普通构建没有超出规定内存预算的输入上，普通构建与加入错误检测工具的构建都不会到达所定义的错误状态，而且具有相同的可观察行为。
这里有一个容易遗漏的限制：这类一致性命题并不排除无限运行。仓库明确说明，当前发布没有证明终止性命题，因此不能把不触发错误改写为程序一定正常结束。这也限定了如何理解公告中关于程序正常退出的概括性描述。
仓库称证明使用Rocq 9.2.0检查，并提供了定理、构建来源和检查工具，便于外部复查。但公开核验路径不等于已经完成独立复现；本报道未运行证明检查器，也未重新执行全部实验。
能否成为日常工程工具，仍取决于成本与复用
此次工作与AI把数学论证写成机器可检查证明的研究有共同思路：生成过程可以复杂甚至容易出错，但最终结果交由独立的形式系统检查。此前本站关于Claude形式化费马大定理的报道涉及Lean中的数学证明；这次的对象则是实际软件二进制及其运行环境，机器模型是否准确因而成为额外的核心问题。
生成大规模软件证明仍然昂贵。Anthropic表示，证明可能消耗数亿个token。在其36个小型验证任务实验中，代理共享证明后，token用量比独立工作减少17%。这说明复用可能降低成本，但并不能据此推算所有项目都会获得同样收益。
Theorem的OSS Verify计划正向符合条件的开源项目免费提供验证服务，优先考虑广泛使用的关键基础设施。项目需要由核心维护者申请，逐项审核；构建还须适配静态riscv64程序，证明生成可能需要数日。免费并不意味着任意仓库可以立即得到完整安全证明。
这项研究的价值，不是宣布软件安全问题已经解决，而是展示一条更具体的工程路线：把安全要求写成明确命题，让AI生成证明，再让外部检查器核验。它能否从研究示范走向日常开发，仍取决于部署环境模型的覆盖、规格质量、证明维护和生成成本。对于开发者，首先要问的也不应只是有没有证明，而是证明了哪个构建、哪条性质，以及在什么条件下成立。