一、先把数字口径对准

2026 年 10 月 22—23 日，Anthropic 研究页（前沿红队 × Theorem Labs）公布了一组实验数据，公开报道里流传的”1.8 亿行”就出自这里。原始口径是这样的：

项目 数值
被测对象 123 个 OSS-Fuzz 开源库中的 239 个入口点
生成证明总量 约 1.8 亿行 Rocq 机器可核验证明
单个典型证明 约 60 万行，对应中位约 18,000 条指令
验证对象 编译后的 RISC-V 机器码，不是源码
待证性质 输入小于 64MiB 时不崩溃、不越界
结果 过程中发现并修复了数百个 bug

还有一组容易被混淆的数字：2026 年 9 月那个”1300 万行 Lean、11 天、60 亿 token”的项目是费马大定理形式化，与本次不是同一件事，两组数字不能互相替代。

最值得注意的其实是最后这组对照实验：在预埋 bug 的随机测试里，传统随机测试漏掉了 7 个中的 5 个，而证明路径把它们抓出来了。这才是”机器码级验证”相对 fuzzing 的真实增量——不是”更聪明”，而是它给的是覆盖性论证，不是抽样。

机器可核验证明与随机测试的覆盖差异

二、为什么这件事对工程有意义

过去形式化验证落不了地，卡点从来不是理论，而是成本：写一份机器可核验的证明，人力成本比写被测代码本身高一个数量级，所以只有航空、芯片指令集、密码学内核这类”错了就完蛋”的模块才配得上。

模型把这部分劳动变便宜了。60 万行证明不可能人工写，但机器可核验这个属性保留了形式的价值——证不对就是证不对，编译器不骗人。这和”AI 生成的代码看起来对”是两种完全不同性质的输出，后者无法自证。

顺带一个副作用很有用：为了让证明通过，模型必须把”这段代码在假设什么”显式写出来。这些假设本身就是最好的安全边界文档，而文档恰恰是企业项目里最先腐烂的东西。

三、它挡不住什么

陶哲轩在其博客（2026-10-09 转载讨论）里点出的那条限制必须一起说清：Rocq、Lean 的内核自身可靠性仍是一个未被证明的猜想。也就是说，”已验证”表达的是”在内核可信的前提下逻辑闭合”，而不是”绝对正确”。

再加上几条工程侧的现实边界：

  1. 证明的是性质，不是意图。 这里证的性质是”不崩溃、不越界”，而不是”业务逻辑符合需求”。一个把订单金额算反的函数，可以完美通过这类证明。
  2. 验证对象是机器码，输入边界是 64MiB。 超出这个尺寸的输入不在承诺范围内，”超过阈值会怎样”要自己兜。
  3. 成本仍然显著。 1.8 亿行证明的背后是可观的算力开销，把它套到全部代码上，任何企业都会被账单劝退。
  4. 入口点数量有限。 239 个入口点相对整个开源生态是选择性的，选哪些入口本身依赖人的判断。

四、企业侧现在能做什么

站在洹拓科技做 AI 模型研发和系统交付的位置，我们把这套方法拆成三档可执行的动作：

档位 做法 适用
立刻可用 让模型生成带断言与前置条件的代码与测试，把”假设”写进仓库 所有项目，成本几乎为零
值得投入 对解析器、加解密、金额计算、上传下载等边界敏感的模块做性质化测试 + 覆盖率与异常用例双轨 有外部输入面的服务
谨慎评估 引入 Lean/Rocq 等可核验工具链，只对少数关键模块做 安全等级要求高、且有专人维护的团队

同时要更新验收口径。我们给客户写交付标准时，会把”AI 辅助”分成两个层次：

  • 生成层（代码、注释、测试用例）：必须过人工评审 + 现有测试，不能因为”AI 写的”就免审
  • 论证层（形式化证明、机器码级检查）：可核验性才是它的价值，验收时应要求给出可复跑的验证脚本，而不是截图或结论

第二点很实际。现在市面上已经有”AI 自动安全加固”这类说法，判断真伪的标准就一条：它能不能交出一个可核验的产物。只能给出”已加固”结论文字的，本质还是抽样测试换了个说法。

五、我们的服务

洹拓科技可以为新乡及周边企业提供：

  • AI 代码评审流水线搭建：把模型评审接入 CI，明确分层验收规则
  • 边界用例与性质化测试补齐：针对外部输入面（解析、上传、支付）补测试矩阵
  • 模型私有化部署：对不便外发源码的团队，提供本地推理与评审方案
  • AI 辅助开发规范制定：把”哪些能自动通过、哪些必须人审”写进团队制度

信息来源：Anthropic 研究页（formal-verification，2026-10-22/23 公开）、陶哲轩博客相关讨论，检索时间 2026-10-24。数字口径以原始研究页为准。

新乡洹拓科技有限公司，软件开发 · AI模型研发 · 云服务与部署运维。

咨询热线：400-829-9957
地址：河南省新乡市辉县市金城百货四楼

#测试 #大模型 #Anthropic #形式化验证 #代码安全