Anthropic 用 Claude 验证 123 个开源库「零崩溃」：AI 从写代码走向证明代码
2026年10月24日 · AI 安全 / 形式化验证 · 深度解读
一句话结论
*Anthropic 与 Theorem Labs 合作，用 Claude 为 123 个 OSS-Fuzz 开源库、239 个入口点生成了机器可检查的正确性证明，覆盖 64MB 以内输入的「永不崩溃」性质——这是 AI 第一次系统性接管了软件工程中最难被自动化的一环：证明而非测试。*
一、核心成果
- 证明覆盖 123 个 OSS-Fuzz 库的 239 个入口点
- 保证：任意输入（不超过 64MB）下都不会崩溃
- 证明运行在编译后的 RISC-V 指令层面
- 证明规模约 1.8 亿行 Rocq（Coq 的继承者），单个证明典型长度约 60 万行
- 过程中发现了多年未被检出的 bug——尽管 OSS-Fuzz 已跑过数万亿次测试
二、为什么这件事是里程碑
*测试只能证伪，验证才能证真。*
传统模糊测试（fuzzing）的逻辑是：不断喂随机输入，看会不会崩。跑一万亿次不崩，不等于「不会崩」——它只把概率压低。而形式化证明给出的是无条件的数学保证。
这次工作把「证明」这件通常需要博士级人力、数月手工建模的事，变成了可由模型规模化执行的任务。Anthropic 的 Frontier Red Team 先让 Claude 自动编写和验证代码：把崩溃测试转换成数学命题，分析编译后的机器代码，再生成广泛证明来验证现有软件。
更值得注意的是，证明过程本身发现了 OSS-Fuzz 漏掉的 bug——那些在数万亿次随机测试中幸存、在几十年维护史里潜伏的缺陷。这说明 AI 在形式化验证上的能力已经超过了传统的随机测试基线。
三、Anthropic 自己划的边界（这点比结果更重要）
Anthropic 在报告中非常坦诚地标注了适用范围的狭窄：
- 证明仅覆盖单线程、静态链接的 RISC-V 二进制
- 链接的是 musl libc，而非 glibc
- 而绝大多数人实际在 x86 或 ARM 上跑这些库，且动态链接 glibc
- 「一个证明只能保证它所证明的性质，规格说明里的任何缺口依然是缺口」
这句话是整篇报告的精髓：**形式化验证的价值上限，取决于规格说明本身是否完备。** 证明了「输入不超过 64MB 时不崩溃」，但如果真实世界还允许 100MB 输入，那么这个证明对生产环境就是零价值的。
Anthropic 同步释放了部分证明以及底层的 RISC-V 与操作系统语义，供第三方独立验证。
四、对行业的三点启示
*1. AI 正在进入「验证层」而非只是「生成层」*
目前 AI 在软件开发中的角色主要是生成代码。但代码生成量激增带来的直接后果是审查瓶颈——人眼看不过来。Claude 这类系统提供的正是补位能力：不是「帮你写得多」，而是「帮你证明它对」。
*2. 安全关键行业的准入门槛会重新定义*
汽车、航空、工业控制等领域的软件认证，长期依赖昂贵的形式化验证人力。AI 把这个成本打下来一个数量级，意味着未来「有形式化证明」可能从「加分项」变成「准入项」。
*3. 与 Anthropic 自我披露的 AI 失控事件形成有趣对照*
同一天，Anthropic 也在另一件事上被审视——其新模型因类似风险开始限制访问实时互联网。一边是模型行为难以预测、难以约束；另一边是模型能力强到能接管最难被形式化的工程任务。能力与对齐的剪刀差正在同时扩大。
五、值得留意的开放问题
- 证明的可维护性如何？60 万行证明在需求变更后如何演进？
- 从 RISC-V/musl 迁移到 x86/glibc 的移植成本有多大？
- 形式化验证的规格说明由谁写？这仍是一个尚未被 AI 充分攻克的瓶颈——AI 能证明「这个实现符合规格」，但规格本身对不对，仍需人类判断。
本文为逍遥云初 AI 科技前沿快讯 · 2026-10-24 · 下午档
