AI 热点快报：Claude 在机器码层面证完 123 个开源库，形式化验证开始按 token 计价（2026-10-24）
事件与背景
2026 年 10 月 22 日，Anthropic 的 Frontier Red Team 发布研究：在与形式化验证公司 Theorem 的合作中，Claude 为 123 个 OSS-Fuzz 开源库、239 个 fuzz 入口生成了机器检查的证明，结论是这些入口「对任何小于 64MB 的输入都不会崩溃」。按原文说法，这是首次把 AI 形式化验证大规模用在生产软件的汇编代码层，而不是重写过的模型代码或教学示例。
关键在证明的对象：不是源码，而是编译出来的 RISC-V 指令。做法是把库里已有的 fuzz test 改写成一条定理——「这个测试对任意输入都不会失败」——再用 Theorem 提供的 RISC-V 指令语义与 Linux 进程语义（LPS）把它翻译成数学模型，由 Claude 写 Rocq 证明，最后交给 Rocq 内核机械检查。规模上，这些证明合计约 1.8 亿行 Rocq，典型一份约 60 万行，而被证明的二进制中位数只有 1.8 万条 RISC-V 指令——证明比代码大一个数量级以上，这正是过去只有空客航电这类项目才养得起的原因（seL4 内核 2 人年写完、20 人年才验证完）。
有意思的是过程产出：为了完成证明，Claude 必须先修掉挡路的 bug。它找到一个解压器的计数器下溢导致写越界，但只在约 20MB、且布局极罕见的输入上触发；一个图像解码器的读越界需要 64MB 输入和超过 2GB 内存；另一个读越界要跨两个指向同一文件的句柄按特定顺序调用；还在 libexpat 里重新发现了 CVE-2026-56132。原文提到，在验证一个广泛使用的 PDF 阅读器时，一周内发现的安全 bug 数量相当于平时一年的报告量。这些都不是「跑得不够久」的问题——fuzzer 的输入上限通常只有 1MB，靠覆盖率引导，天生到不了这些角落。
来源（均已用 curl 验证返回 200）：
- LLMs are making formal software verification feasible at a much larger scale — Anthropic，2026-10-22
- OSS Verify: proofs about OSS-Fuzz fuzz targets — theorem-labs/oss-verify-proofs（公开证明仓库）
- OSS Verify — Theorem：面向合格开源项目免费，按 OSS-Fuzz 的方式提交 PR 登记
- add-project SKILL.md：Theorem 发布的 Claude skill，教 agent 给自己的项目接上验证流水线
- OpenShell — NVIDIA 的 agent 运行时，策略变更前用形式化验证预演会放开哪些权限
为什么现在重要
1. 验证的单位从「源码」换成了「二进制」，语言和构建系统不再是门槛。 只要能被编译成 RISC-V 静态二进制，C、C++、Rust、Go 写的库走同一套流程；Anthropic 另外还示范了直接对 x86 二进制证明 zlib 符合 RFC 1950。影响：依赖审计可以对你实际部署的产物做，而不是要求上游先把代码重写成某个验证友好的语言。
2. 成本曲线第一次有了可读的斜率，而这决定它能不能进 CI。 原文承认证明可能消耗「数亿 token」，但同时给出两组数字：在 36 个真实 OSS-Fuzz 小任务上，Opus 5.5 用比 Opus 5 少约 40% 的 token 证完其中一半；让 agent 共享已完成的证明后，token 再降 17%，还有两个原本失败的 agent 因此成功。影响：把「一个入口一份证明」当预算项排进季度计划，比排「一位形式化方法专家」现实得多。
3. 信任基座被压缩成一份可以点名的清单。 需要信的只剩四样：RISC-V 语义、Linux 进程语义、被证明的定理陈述原文、Rocq 检查器本身（严格说还有跑检查器的硬件与 OCaml 编译器）。影响：安全评审的问法要改——从「你测了多少覆盖率」变成「你的 trusted base 是哪几个组件、定理陈述的输入上界是多少」。
4. 同一周，形式化验证已经出现在 agent 基础设施的默认件里。 NVIDIA 的 OpenShell 用内核级沙箱限制每个 agent 能碰的文件、系统调用和网络，并在策略变更生效前用形式化验证标出「这次改动会新放开哪个主机、哪条 API」等待人工复核。影响：做 agent 平台的团队，权限审批可以从事后 review diff 变成事前证明「新增了什么能力」。
5. 但「已验证」离「没 bug」还有三段距离，Anthropic 自己写清楚了。 其一，模型不等于真机：证明假设单线程、静态链接 musl、固定内存预算的 RISC-V，而生产环境多是 x86/ARM + 动态链接 glibc；其二，定理范围有限：ASan 检不到全部内存错误，也没覆盖每个库的所有入口，库内死代码与调用方的误用在证明之外；其三，公开的证明只是子集——仓库目前写明 25 个库、60 个入口，而文章说的是 123 个库、239 个入口。影响：任何对外宣称都要带上前提，否则就是把一份有边界的保证卖成了无限责任。
工程师/产品人今天能做什么
- 挑一个你真正依赖、且已有 fuzz target 的库，只证一个入口。 走 Theorem 的 OSS Verify 登记流程（对合格开源项目免费），或照 add-project skill 在本地跑；目标不是「全库验证」，而是先拿到一份能通过的证明，量一下 token 与时间。
- 把「fuzz test 永不失败」当成 spec 来写。 定理的形式是「这个 crash 条件在任意输入上都不成立」，所以测试写得越贴近你关心的性质（往返一致、幂等、与参考实现等价），证明的价值越高；纯内存安全的入口是最低门槛起点。
- CI 里分开两件事：生成证明（贵、可缓存）和检查证明（便宜、确定性）。 Rocq 内核检查是机械的，适合每次构建都跑；而重新生成证明应按需触发，产物入库。这条分工直接决定验证能不能长期维护。
- 给安全评审模板加一栏 trusted base。 要求列出：检查器版本、语义模型版本、定理陈述原文链接、覆盖的输入上界、以及明确排除的范围（线程模型、动态链接、调用方契约）。缺这栏的「已形式化验证」不予采信。
- 别在对外材料里省略前提。 参照原文的 Limitations 写三条：模型与真实机器的差距、定理覆盖不到的部分、调用方必须遵守的约束。这既是诚实，也是出事时的责任边界。
待观察
- 公开证明与论文数字的缺口。 仓库当前是 25 库 / 60 入口，且明确说「不公开可能暴露未修补 bug 的证明」。其余部分何时放出、扣下了多少，是判断这次成果可复现性的关键。
- x86 与动态链接的语义何时可用。 原文把「为 x86 生成准确语义」列为下一步；这一步不通，绝大多数生产部署仍落在证明假设之外。
- 社区的两条质疑还没被回答。 HN 上的高赞评论集中在两点：这种冗长证明风格遇到更复杂程序会不会撞上复杂度墙（原文附录自己也引了 MachCSL 的经验），以及 spec 是否符合人的真实意图——证明检查器不会告诉你「你证的定理是不是你想证的那条」。
- Theorem 的 Nix 生态路线图（glibc、OpenSSL、cURL）能否按包粒度复用证明。 依赖是幂律分布的，这条路若成立，验证成本会被摊薄到整个生态；目前只有路线图，没有公开的成本数字。