发生了什么
Anthropic 前沿红队与形式化验证公司 Theorem 在 10 月 22 日公开了这项合作：把 Google OSS-Fuzz 里已有的模糊测试用例直接当作规格来源，让 Claude 为编译后的 RISC-V 二进制编写机器可检查的证明。数周内完成 239 个入口点、覆盖 123 个开源库，全部证明由 Rocq 证明助手的内核逐条核验。
方法论上最关键的一步是「改写命题」。模糊测试只能反复抽样，永远无法回答「没有漏洞」；这项研究把每个 fuzz 入口点转成一句话：对任何小于 64MB 的输入，程序都不会崩溃，也不会触发内存安全错误或断言失败。规格建立在 Theorem 提供的 RISC-V 指令语义与 Linux 进程语义之上，Claude 负责写证明，Rocq 负责判定证明是否成立。
- 共 239 个 fuzz 入口点，来自 123 个 OSS-Fuzz 开源库
- 通过检查的证明约 1.8 亿行 Rocq；团队称 Claude 实际写过约 10 亿行
- 单条典型证明约 60 万行，对应二进制中位数 1.8 万条 RISC-V 指令
- cJSON 一个 391 行的解析器，生成了 63 万行证明
- 公开仓库首版只放出 60 个入口点、25 个库的证明，是完整研究的子集
证明过程中挖出的漏洞
比证明数量更有信息量的是沿途结果。这些库都已在 OSS-Fuzz 上跑过海量测试，证明过程仍翻出数百个缺陷，而且多属于模糊测试难以命中的形态。
- 某解压器副本的计数器下溢，只在约 20MB、内存布局罕见的输入上触发越界写
- 某图像解码器的越界读，需要 64MB 输入并占用 2GB 以上内存
- 在 libexpat 中重新发现 CVE-2026-56132；还发现一类不导致崩溃、但未按预期限制文件加载的逻辑缺陷
- 团队称验证某广泛使用的 PDF 阅读器时，一周内发现的漏洞数量相当于该项目平时一年
信任边界与真实代价
形式化验证的可信度取决于假设。这条链路里只需相信三样东西：RISC-V 与 Linux 进程的形式语义、定理陈述本身、Rocq 检查器内核；Claude 的推理不进入信任基。代价同样明确：有单条证明的检查在 16 核上要吃掉最多 20GiB 内存，模型侧的 token 消耗以亿计。
覆盖范围也写得很死：单线程、静态链接、RISC-V、musl libc、固定内存预算。真实部署大多跑在 x86 或 ARM、动态链接 glibc，这些结论不能直接平移；AddressSanitizer 本身也覆盖不到全部内存安全缺陷。Anthropic 自己的措辞是「形式化验证不等于没有 bug」，规格写错，证明再漂亮也无效。
- 在 36 个缩小规模的验证任务上，Opus 5.5 完成一半，token 消耗比 Opus 5 少约 40%
- 多个智能体在共享工作区复用彼此的证明，token 再降 17%，部分原本失败的智能体借此完成任务
- Theorem 通过 OSS Verify 计划向开源项目免费开放流水线，报名方式是提交一个 pull request；路线图指向 Nix 生态，先做 glibc、OpenSSL、cURL
对企业采购意味着什么
供应链安全报告的证据形态正在变。过去交付的是扫描报告与渗透结论，现在可以附上「定理陈述 + 二进制哈希 + 编译器版本 + 可复现的检查器镜像」，让对方自己跑一遍检查。采购与安全团队真正要追问的不是「是否已形式化验证」，而是覆盖了哪些入口点、假设了什么执行模型、公开了多大比例的证明。按目前的进度，多数商业软件还拿不出这套材料，但把它写进 2027 年的供应商问卷并不算早。