Anthropic与Theorem公布AI形式化验证成果：证明覆盖到哪里？

AI编程助手能够改代码之后，下一步能否交付可以被机器检查的安全证据？10月22日，Anthropic与Theorem公布合作成果：用Claude为真实开源软件的部分编译产物生成形式化证明。值得关注的变化，是开发流程开始把“写出代码”和“给出指定性质的证明”连接起来。但判断这项成果的价值，需要同时看研究规模、公开材料和证明边界。

背景：测试寻找反例，证明检查明确的命题

模糊测试会不断构造输入，寻找崩溃或断言失败。形式化验证则先把需要保证的性质写成精确规格，再证明它在约定条件下成立。此次路线围绕既有测试入口，把“某类输入不会触发指定错误”转为可由Rocq证明检查器核验的命题。AI负责生成证明，检查器按规格核对，二者承担不同角色。

这里的“规格”非常关键。如果团队只规定不能出现某类内存错误，就不能顺势推出业务结果一定正确。对中文开发者而言，这让安全讨论有了一个更具体的问题：交付物究竟承诺了哪个入口、哪种构建、哪项性质？

研究规模与公开证明要分开读

Anthropic公告称，团队在修补发现的问题后，为123个OSS-Fuzz开源库中的239个入口完成了相关证明。公告同时说明，只公开其中一部分材料。截至本次核查，Theorem公开仓库README列出的是25个库、60个入口。前者是研究方报告的整体范围，后者是本次可以定位到的公开证明子集，两组数字不能相互替代。

公开仓库还提供构建记录、二进制校验与检查流程。读者可以据此追踪证明对应的具体产物，而不是仅凭项目名称判断自己的软件已经得到覆盖。本文核查了文档与公开材料，未自行重跑整套证明。

边界：特定构建、系统模型和错误类型

该路线针对静态链接的RISC-V二进制，在单线程、固定内存预算等约定下建模；项目说明把输入上限写为64 MiB。公开仓库明确指出，证明针对某个入口能够到达的代码及指定构建，不自动延伸到整个库、其他版本或x86-64构建。

同样需要看Linux进程语义模型LPS。仓库说明该模型并不完整，仍有假设。公开材料也不排除检测器无法发现的错误结果或内存泄漏；本次公开证明没有证明终止性，因此不能把它写成“任何输入都保证及时正常退出”。这些限制决定了证明可被采用到哪一步。

对开发流程的影响：证据可以跟随交付物

编辑部认为，近期更现实的用途是把高风险解析器、压缩组件等明确入口纳入验证试点。团队应保留二进制哈希、上游提交、构建参数、规格和检查器版本，让后续版本升级能够触发复核。证据与实际部署产物对应，才方便在发布和审计环节使用。

企业仍需用测试、代码审查与运行监测覆盖规格之外的问题。AI降低写证明的门槛，并不免去工程团队定义正确目标和评估系统假设的责任。

适合哪些人关注，怎样开始

开源基础库维护者、软件供应链安全团队，以及拥有可复现构建的研发组织值得跟进。Theorem的OSS Verify面向符合条件的开源项目免费提供验证，申请由核心维护者通过项目仓库提交，是否接纳需要审核；这不是任意代码上传后立即获得证明的通用免费服务。

一个可执行的起点是：挑选单一入口，确认静态RISC-V构建可行，列明要排除的错误，再评估迁移、计算资源与持续维护成本。先让一项安全主张可被复核，再讨论扩大范围。

来源参考

• Anthropic：形式化软件验证研究公告（2026年10月22日）
• Theorem：公开证明仓库与适用范围（本次核查快照）
• Theorem：Linux进程语义模型及限制
• Theorem：OSS Verify开源项目申请说明