Anthropic：Claude 为 123 个开源库生成机器检查的安全证明

Anthropic 前沿红队与 Theorem 合作，把开源库现有的 fuzz 测试转成形式化规格（任何小于 64 MB 的输入都不会让 fuzz 入口崩溃），由 Claude 在 RISC-V 汇编层面编写证明，再由 Rocq 证明检查器验证。几周内完成了 123 个库的 239 个入口，过程中发现并修补了数百个 bug。

要点

• 证明总计约 1.8 亿行 Rocq，典型证明约 60 万行，对应中位数 18,000 条 RISC-V 指令的二进制
• 发现的问题包括只在约 20 MB 罕见输入下触发的越界写，并重新发现了 libexpat 的 CVE-2026-56132
• 为防止「改程序让定理变好证」，团队对补丁扣分、记录并审计所有补丁；36 个小任务中 Opus 5.5 证完一半所用 token 比 Opus 5 少约 40%
• 局限：证明假设单线程、静态链接 musl 的 RISC-V 程序，而多数实际部署是 x86/ARM 加 glibc 动态链接；「形式化验证」不等于没有 bug

来源

### [Anthropic：Claude 为 123 个开源库生成机器检查的安全证明]({{URL}})

Anthropic 前沿红队与 Theorem 合作，把开源库现有的 fuzz 测试转成形式化规格（任何小于 64 MB 的输入都不会让 fuzz 入口崩溃），由 Claude 在 RISC-V 汇编层面编写证明，再由 Rocq 证明检查器验证。几周内完成了 123 个库的 239 个入口，过程中发现并修补了数百个 bug。

- 证明总计约 1.8 亿行 Rocq，典型证明约 60 万行，对应中位数 18,000 条 RISC-V 指令的二进制
- 发现的问题包括只在约 20 MB 罕见输入下触发的越界写，并重新发现了 libexpat 的 CVE-2026-56132
- 为防止「改程序让定理变好证」，团队对补丁扣分、记录并审计所有补丁；36 个小任务中 Opus 5.5 证完一半所用 token 比 Opus 5 少约 40%
- 局限：证明假设单线程、静态链接 musl 的 RISC-V 程序，而多数实际部署是 x86/ARM 加 glibc 动态链接；「形式化验证」不等于没有 bug

**为什么值得关注**：形式化验证一直因人工成本过高难以推广，这项工作说明 LLM 可以把它扩展到大量真实代码上；证明仍需数亿 token，但部分证明、语义模型和登记工具已经开源。

来源：[LLMs are making formal software verification feasible at a much larger scale](https://www.anthropic.com/research/formal-verification)；[HN discussion](https://news.ycombinator.com/item?id=50202217)