Anthropic 前沿红队 10 月 22 日发布研究，用 Claude 给 123 个开源库的 239 个入口点写出了形式化证明：只要输入小于 64 MB，这些程序都不会崩溃。证明直接落在编译后的 RISC-V 可执行文件上，合作方是做形式化工具的 Theorem。Anthropic 称，这是 AI 第一次在生产软件的汇编层面大规模做形式化验证。
这批库全部来自谷歌的 OSS-Fuzz 项目，也就是长期挂在模糊测试平台上的那一批基础组件，压缩、图像解码、HTTP 解析都在里面。整个工程用了几周。
把模糊测试改写成定理
做法分三步。第一步，团队把每个库已有的 fuzz 测试套件改写成一条形式化规约，意思是”这段测试代码对任意输入都不崩溃”。规约建立在 Theorem 提供的 RISC-V 指令语义和 Linux 进程语义模型之上。
第二步交给 Claude 写证明，再由 Rocq 证明检查器逐条核对。
“Claude writes the proof; the Rocq kernel checks it against the specification.” （Claude 写证明，Rocq 内核拿它去对照规约检查。）
第三步处理证不下去的情况。证明卡住，往往说明代码里真有缺陷，这时 Claude 自己改代码，规约重新生成，再接着证。团队承认这一步容易出现”奖励黑客”，模型可能为了让证明通过而乱改程序，所以给补丁加了惩罚项，要求证明补丁影响的输入范围，并逐条记录、人工审计。
一份典型证明约 60 万行。最终需要信任的部分只剩 RISC-V 和 Linux 的语义模型、定理陈述本身和 Rocq 检查器。
证明过程中挖出的漏洞
证明途中发现并修复的漏洞有数百个，其中一些很难靠模糊测试撞出来。文章举了几例：一个解压器的计数器下溢，只在约 20 MB 的特定输入下触发；一个图像解码器的越界读，要 64 MB 输入加 2 GB 以上内存才会出现；还有一个越界读需要两个句柄按特定顺序操作同一文件。libexpat 的 CVE-2026-56132 也被重新发现了一遍。
cpp-httplib 的证明多了一道坎：std::set 析构时的递归可能导致栈溢出。为排除这种情况，团队在机器码层面证明了 libc++ 红黑树的平衡算法能把树深度压在对数级别。
同一篇研究还附了几个旁支实验。Claude 用 Rust 写了一个 Python 子集，并用 Verus 证明它符合 CPython 语义，在 170 万个随机程序上与 CPython 行为一致的比例为 99.95%。它还自己生成了一套 x86 指令语义，单步执行能启动 Ubuntu 用户空间，顺带查出官方参考文档里数百处错误。
拿 seL4 对照着看
形式化验证在工业界并不新鲜，难处一直在人力。业内常拿 seL4 微内核举例：大约一万行 C 代码，当年的证明投入通常被引述为二十人年左右。CompCert 编译器走的也是类似路线，靠一支小团队多年打磨。这类项目的共同点是对象少、周期长、专家密集。
Anthropic 这次的规模是 123 个库、几周时间，粗略对照，单位工作量的成本结构已经换了一种形态，人从写证明退到定规约、审补丁。代价换成了 token：文章说一份完整证明可能要消耗数亿 token。在 36 个小型任务上，每个任务给单个 agent 三次尝试、每次 500 万 token 预算；允许 agent 复用彼此的证明后，所需 token 又降了 17%。
两边的保证强度也不在一个层级。seL4 证的是功能正确性，这次证的只是”不崩溃”，范围窄得多。
证明之外的空白
Anthropic 自己列的局限相当具体。证明基于单线程、静态链接、使用 musl libc 的 RISC-V 二进制，而大多数用户实际跑的是 x86 或 ARM 上动态链接 glibc 的版本。AddressSanitizer 本身抓不到所有内存安全错误，也有入口点没被覆盖，调用方误用库导致的内存损坏同样不在证明范围里。
""Formally verified” does not mean “bug-free."" （“形式化验证”不等于”没有 bug”。）
规约和真实机器之间的偏差，是这条路线最容易出事的地方。Rocq 和那几套语义模型本身也要加固，文章说这件事”不是小事”。团队给出的判断是，形式化验证会成为安全软件开发的常规环节，至于这些证明何时能覆盖到 x86 和 glibc 这类主流部署环境，文章没有给出时间。
参考来源：Anthropic 前沿红队研究文章、CocoLoop；Anthropic 研究页核验库数量、入口点数、证明行数与 token 对比口径。