形式化验证推荐解读，AI 开始替程序写数学证明了
测试证明不了软件没 bug，只能证明有 bug，这句行业老话的另一半解法叫形式化验证，用数学定理证明程序满足规约，规约写清楚，证明机器查，谁也糊弄不了谁。这条路贵到只有航天与内核这种要命的场景才用得起。十月二十二日 Anthropic 发了一篇研究，宣称大模型把这件事的规模推上去了。我核了研究原文与 HN 讨论，成绩惊人，自称口径也密集，拆开看。
研究做了什么
先纠正一个流传中的细节，用的证明器是 Rocq，就是当年那个老牌证明器改的名，不是另一家，改名换姓不影响内核扎实。这次主战场在汇编层，团队选了模糊测试项目开源库做对象，让 Claude 对 RISC-V 架构二进制直接生成证明，处理器指令集语义模型也由模型自主生成。验证对象一百二十三个开源库、二百三十九个入口点，配了另一套工具链验证一个 Rust 写的解释器，两套战场互为犄角。全部数字出自官方，自称口径。
成绩单
自称的数字先摆出来。生成约一亿八千万行证明，单个证明典型六十万行。覆盖所有小于六十四 MB 的输入，对照模糊测试通常只测一 MB 上下的样本，这是证明与采样的本质差别。发现了数万亿次模糊测试都没摸到的漏洞，包括一个要约二十 MB 特定布局输入才触发的越界写，和一个潜伏十余年的逻辑错误，还在一个解析库里重新发现了已知编号漏洞。Rust 解释器经一百七十万个随机程序对照，与官方实现行为一致率百分之九十九点九五。
老办法贵在哪
传统形式化验证的账本摆在那里，某个著名微内核实现花两人年，验证花二十人年，十倍的工程放大让这门手艺常年困在象牙塔。模糊测试走的是另一条路，撒点抽样，便宜但覆盖不了长尾，二十 MB 的触发条件就是它够不着的那种。这篇研究的卖点正是用模型把写证明的人力成本打下来，让验证从人年变成机时。证明还有个复用红利，依赖关系呈幂律分布，底层的证明攒下来，上层项目接着用，用得越多攒得越厚，这门手艺第一次有了复利。
局限写得诚实
原文自己承认的部分要完整转述。通过形式化验证不等于没有 bug，规约本身可能写错，机器语义模型也可能错。覆盖面目前限单线程、静态链接的 RISC-V 二进制，真实世界主流的架构与动态链接还没碰。入口点没验完，单个证明要烧数亿 token，还有模型投机取巧的风险。这份局限清单本身就是研究可信度的加分项。
HN 怎么看
讨论串七十多分。支持方带着实例来，有人分享用同样思路验证 Rust 重写版数据库，已覆盖约一成二代码，有人展示代理提交代码时附上机器可查的等价性证明，这条工作流被普遍认为是最接近落地的方向。质疑方也不客气，有人说大模型擅长插值拙于外推，冗长证明会撞上复杂度墙，有人翻出历史上证明通过但结论与论文不符的先例，还有人一句总结，自己给自己写测试当然全过。两边的共同点是都承认方向有价值，分歧在墙有多远，墙的位置要靠更多实战项目去撞。
解决了什么需求
对普通开发者，这项研究暂时用不上，工具链面向特定架构且成本高昂。但它指出的那条路离生活不远，代理提交代码附带机器可查的证明，评审从读代码变成验证明，这个工作流已经有团队在用。对安全行业，长尾漏洞的挖掘多了一件重武器。看热闹的读者记住一个趋势就够，AI 的下一个战场在正确性，写代码之后是证代码。
一句收尾，测试找的是存在 bug，证明排除的是可能 bug，后者终于开始变便宜，便宜到普通项目也敢想。
来源
- 研究原文 https://www.anthropic.com/research/formal-verification
- HN 讨论帖 https://news.ycombinator.com/item?id=50202217
- 证明开源仓库 https://github.com/theorem-labs/oss-verify-proofs