Anthropic 用 Claude 给 123 个开源库做“不会崩溃”的数学证明：条件是 RISC-V、单线程、输入不超过 64MB
zovo约 3 分钟读完
Anthropic 前沿红队在 10 月 22 日发布研究：与 Theorem 公司合作，让 Claude 为 123 个开源库写出数学证明，证明其中 239 个测试入口在一组明确假设下，面对任何小于 64MB 的输入都不会崩溃。以往这类证明靠专家逐行手写，成本高到只有航空电子这类关键系统才用得起。
01它到底证明了什么
模糊测试（fuzzing）是给程序喂海量随机输入、看会不会崩溃，但输入是无穷的，永远测不完。Anthropic 的做法是把开源库现成的模糊测试入口当成“规格”：编译成 RISC-V 机器码后，要求 Claude 证明这个入口对任何小于 64MB 的输入都不会崩溃、不触发内存安全错误或断言失败。证明由 Rocq 证明检查器机械核验，人不需要逐行审。
| 项目 | 官方披露 |
|---|---|
| 覆盖范围 | Google OSS-Fuzz 中 123 个库、239 个入口 |
| 证明层级 | 编译后的 RISC-V 汇编（可执行文件），不是源码 |
| 体量 | 约 1.8 亿行 Rocq，单个证明约 60 万行 |
| 耗时 | 几周 |
| 输入上限 | 64MB（官方称调大只需改参数并重新证明） |
02过程中挖出的 bug
证明失败的地方往往就是 bug。Claude 先修补再证明，官方称发现了数百个 bug，其中有些模糊测试很难碰到：比如某解压库里一个计数器下溢，只在约 20MB、特定布局的输入上触发越界写；某图像解码器的越界读需要 64MB 输入和超过 2GB 内存；还重新发现了 libexpat 的 CVE-2026-56132。为防止 Claude 靠“把程序改成永不崩溃”来投机，官方对每个补丁扣分并事后审计。
03别把“证明过”当成“没 bug”
官方自己写了限制，这是读这篇研究最该留意的部分：
- 证明只对单线程、静态链接、固定内存预算、运行在 Linux 的 RISC-V 二进制成立；多数人实际跑的是 x86 或 ARM、动态链接 glibc。
- ASan 查不到所有内存错误，也没有验证每个库的所有入口，调用方误用库造成的问题不在范围内。
- 需要信任的只剩三样：RISC-V 与 Linux 进程的形式化模型、定理陈述本身、Rocq 检查器。剩余 bug 只可能在这些之中或证明范围之外。
04成本与可复用性
官方承认单次证明可能消耗数亿 token。他们在 36 个小任务上测得，Opus 5.5 证明一半任务所需 token 比 Opus 5 少约 40%；让多个智能体共享已完成的证明，平均少用 17% token。这些均为 Anthropic 自测。
05对开发者意味着什么
Anthropic 公开了部分证明和 RISC-V/Linux 语义（theorem-labs/oss-verify-proofs），Theorem 也提供为其他开源项目跑同一流程的服务，并发布了一个帮助开发者上手的 Claude skill。本站未运行这些证明或工具。对维护开源库的人来说，已有模糊测试的项目最有可能受益；对普通使用者，短期内不会看到“已验证”标签，但这类证明让依赖库的关键路径有了可复核的保证。
提示读到“形式化验证”时先问两件事：证明的规格是什么，机器模型和真实环境差多远。这篇研究的结论成立于它写明的假设之内。
资料来源（2026-10-23 核对）
本文由 zovo 编辑撰写，转载请注明出处。
Claude Code
Hy-Memory
Octop