Anthropic：Claude 在汇编级为 123 个开源库写出可机器检查的无崩溃证明
Anthropic 与 Theorem 合作发文称，Claude 已在 RISC-V 汇编级为 123 个真实开源库的 239 个入口证明：在单线程静态二进制、固定内存预算、Linux 等假设下，对任意小于 64 MB 的输入不会因内存安全错误或断言失败而崩溃。证明约 1.8 亿行 Rocq，并由外部证明检查器核验。文中强调「形式化验证」不等于「无漏洞」。
Anthropic Frontier Red Team 于 2026 年 10 月 22 日发布研究博文，介绍与 Theorem 的合作：用 Claude 在生产软件的汇编（RISC-V）层大规模生成形式化证明。公司称，这是据其所知首次以 AI 在汇编级对生产开源软件做大规模形式化验证。目标规格由既有模糊测试入口转换而来——证明「该入口对任意小于 64 MB 的输入永不崩溃」（含 AddressSanitizer 捕获的内存错误）。
结果（Anthropic 自述）：数周内 Claude 先修补发现的缺陷，再为 123 个 OSS-Fuzz 库中的 239 个入口完成无崩溃证明；证明总量约 1.8 亿行 Rocq，典型单证明约 60 万行，对应中位约 1.8 万条 RISC-V 指令的二进制。证明依赖 Theorem 的 RISC-V 指令与 Linux 进程语义，当前假设包括：单线程静态二进制、固定内存预算、RISC-V CPU、Linux。公司发布部分可复用证明与语义，Theorem 亦提供为其他开源项目运行同类流水线及 Claude skill。
局限被明确写出：「形式化验证」不等于「无漏洞」。证明只保证编译后程序满足形式规格；若规格或机器模型与真实部署不符（例如多数库实际跑在 x86/ARM 并动态链接 glibc），保证不迁移。ASan 也无法覆盖全部内存安全问题，且未验证每个库的全部入口。文中还提到证明过程中发现多年漏检缺陷（含需约 20 MB 特定布局才触发的写越界等），以及 Claude 生成证明时可修补代码——并以额外约束抑制「改程序使之平凡可证」的奖励黑客。