大模型让形式化验证变得可行了

"这段代码没有内存安全问题"，这句话以前只能靠测试覆盖率来暗示。现在有人把它变成了一道数学题，并且交给模型去解。

一、发生了什么

10 月 22 日，Anthropic 的前沿红队与合作方 Theorem 发布了一份研究，说他们让 Claude 对编译后的 RISC-V 机器码写形式化证明。以下数字均为厂商口径，未经第三方复现。

覆盖范围是 123 个 OSS-Fuzz 开源库、239 个入口点。证明的目标很朴素：对任何小于 64MB 的输入，程序都能正常退出，不越界、不触发断言失败。证明代码总量约 1.8 亿行，单个库通常在 60 万行上下，被验证的二进制中位数是 1.8 万条指令。整个活干了几周。证明最后由 Rocq 检查器机械校验，不需要人逐行读。

配套案例里有几个更能说明问题的：Linux 内核里 zlib 的 x86 二进制，按 RFC 1950 的规格被证明实现正确；一个用 Rust 重写的 Python 解释器，用另一个工具证了与 CPython 语义一致，在 170 万个随机程序上一致率 99.95%；一个 PDF 阅读器在一周内发现的漏洞数量，相当于平时一整年的报告量。文献里还提到重新发现了一个已编号的 libexpat 漏洞，以及一个潜伏十余年的逻辑错误。

二、跟你有什么关系

写 C 或 C++ 的基础库维护者：这条路第一次在成本上有可能摸到。以前形式化验证是航天和芯片团队的专属预算。

做安全的人：漏洞发现的速度变了。以前是一个季度出一批，现在可以按周批量出。你的排期得跟着改。

技术负责人：别急着立项。先看清它证明的是"符合规格"，不是"没有 bug"。这两句话差着一个数量级的工作量。

三、怎么判断

1. 先问规格从哪来。这项工作的做法是把已有的模糊测试改写成命题——测试断言"不许崩"，命题就是"任何输入都不崩"。规格写得对不对，检查器不管。
2. 看被验证的边界。这批结论成立的前提是单线程、静态链接 musl、固定内存预算的二进制。你线上跑的是动态链接的 x86 或 ARM，直接套不上。
3. 查可信底座。RISC-V 和 Linux 的形式化语义模型、定理陈述本身、证明检查器，这几样仍然要靠信任。
4. 防作弊。研究者自己列了风险：模型可能把程序改成永不崩溃来让定理成立。他们的应对是惩罚补丁、要求证明输入的影响范围、留审计日志。你复现时要照抄这三条。

四、三个别信的说法

证明了就等于没有漏洞。 证明只保证在给定规格下成立。规格漏掉的属性，证明一个都不会抓。文章自己写得很清楚：形式化验证不等于无 bug。

模型会写证明了，验证工程师要失业。 恰恰相反，工作量往前挪了。写证明这件事被压到几周，写清楚"什么算对"变成主要成本。规格写错，后面全部白干，而且错得很安静。

这是通用能力，什么代码都能证。 目前公开的成果集中在内存安全这一类属性上，被测程序也有明确的前提假设。业务系统里那些"订单不能重复扣款"的需求，还没有对应的成熟规格写法。

五、一句话结论

证明变得便宜之后，贵的部分是你到底想要什么。

信息来源

• Anthropic：用大模型做大规模形式化验证，2026 年 10 月 22 日

功能与价格以官方公告为准。本文写于 2026 年 10 月 23 日。