2026 年 10 月 22 日，Anthropic 与安全初创团队 Theorem 联合公布了一项进展：研发团队借助 Claude，首次在 RISC-V 汇编层级对 123 个开源软件库的 239 个模糊测试入口点完成了自动化形式化验证。整个验证流水线最终生成并采纳了约 1.8 亿行 Rocq 定理证明代码，期间还挖出了多例连数万亿次模糊测试都未曾触发的深层真实漏洞。
形式化验证曾是计算机科学中最昂贵的理想国。它用严密的数学推演证明代码绝对杜绝特定错误，但在过去，这种保证极度依赖数学与系统工程专家的手工编写。最著名的微内核项目 seL4 仅用 2 人年编写代码，却耗费了整整 20 人年才完成数学证明。Anthropic 此番动作的核心价值，在于第一次用大模型将形式化验证从航天军工与高精加密模块的象牙塔，硬生生拉进了通用开源软件的生产流水线。但这并非软件绝对无错的神话落地，而是一次在高度受限环境下的工程算力突围。
把模糊测试升格为数学定理：暴力推导填平人力天堑
软件开发长期面对一个残酷事实：测试只能证明缺陷存在，无法证明缺陷不存在。工业界此前排查漏洞主要倚仗 Google OSS-Fuzz 这类持续模糊测试平台，通过海量随机变异输入轰击接口。然而盲测存在固有物理上限，通常输入体积上限只有 1 MB 左右，无法穷尽逻辑组合。
Anthropic 采取了一种讨巧却极具工程野心的做法。他们没有试图对庞杂的开源库进行端到端的全局语义建模，而是将开发者在 OSS-Fuzz 中写好的测试桩，直接升格为数学规范：证明在任意小于 64 MiB 的合法输入下，经过地址消毒剂（ASan）或未定义行为消毒剂（UBSan）插桩的程序，绝对不会触发崩溃或内存非法访问。
为了绕过高级语言编译器的未定义行为陷阱，验证没有停留在 C/C++ 源码，而是沉降到底层的 RISC-V 汇编指令。大模型面对的是机器码层级的寄存器状态转移。在整个试验周期中，Claude 生成了约 10 亿行代码进行自我试错与迭代推演，最终沉淀出 1.8 亿行被 Rocq 证明检查器接纳的证明。平均折算下来，单个测试入口点的证明体量就高达 60 万行。
这种穷举式推演展现出传统测试无法企及的排障能力。在推导过程中，Claude 捕获了多起潜伏多年的严重边界漏洞。其中包括一个需要精心构造约 20 MB 特殊排布输入才会触发的解压器计数器下溢写越界漏洞，一个必须喂入 64 MB 数据且吃掉超过 2 GB 内存的图像解码读取越界，同时还重新独立命中了 libexpat 库中已知的深层嵌套漏洞 CVE-2026-56132。这些漏洞在现实世界中往往能避开常规安全防御，成为攻击者手中的高危利用链。
显微镜下的边界：剥开宣传话术后的五重现实围墙
Anthropic 官方博文使用了“程序在特定条件下永不崩溃（always exit normally）”的断言，但仔细审视开源的证明仓库和形式化语义底牌，会发现这套确定性保障背后砌起了严密的前提围墙。
其一，并未证明程序一定会停机。公开仓库明确标注文档缺少停机性命题（halts statement）。这意味着，Claude 证明的仅仅是“程序在执行路径上只要触碰到退出指令，就不会发生内存越界和断言失败”，但它完全没有排查死循环。一个挂死在内部无限循环中导致服务器资源耗尽的拒绝服务（DoS）漏洞，依然能顺利通过该验证。
其二，制品环境处于真空温室。本次验证的所有目标二进制，被严格限定为基于 musl 库静态编译的单线程 riscv64 二进制文件，输入严控在 64 MiB 之内，ASan 证明的内存预算为 2 GiB，UBSan 为 16 GiB。在真实工业界，服务器端绝大多数性能敏感组件都重度依赖动态链接、多线程共享内存和异步事件驱动，而这些复杂的并发状态完全被排除在当前的验证模型之外。
其三，依赖模型的规格漂移风险。底层验证框架依赖一套由 Theorem 编写的极简 Linux 进程语义模型。该模型删繁就简，排除了真实的信号处理机制，并将文件系统和系统调用高度抽象化。证明通过的前提，是这套数学模型与真实硅片硬件、Linux 内核的行为分毫不差。一旦抽象失真，数学上的铁证就会沦为沙盒里的游戏。
机器推导出的确定性，其可靠上限永远受制于它所立足的假设围墙。
- 风险.生产端部署的主流服务器均为 x86 或 ARM 架构，因编译优化与指令排布差异，静态 RISC-V 上成立的汇编证明无法向异构二进制平移。
算力账本与激励扭曲：工业化落地前的商业考量
抛开技术语义的局限，从工程落地和资源消耗视角审视，这项新范式同样面临着算力账本与维护机制的双重压力。
在验证过程中，单个证明最终由 Rocq 内核进行机械复核，在 CPU 上就需要耗费 30 分钟至数小时。如果加上前期由大模型吐出 10 亿行推导代码的试错过程，其背后燃烧的算力成本不容小觑。好消息是推理效率正在陡峭上升：数据显示，在 36 个基准测试中，Opus 5.5 完成一半任务所需的 Token 消耗较 Opus 5 减少了约 40%；如果引入既有证明片段进行复用，还能额外削减 17% 的消耗。
但在经济账之外，最令系统工程师担忧的是“AI 自动修补原代码”带来的激励扭曲。在验证失败时，为了保证流程不断流，系统允许 Claude 自动 patch 原代码，修补完再重新生成规范予以证明。大模型本能的目标是“让定理推导成功通过”，当修复逻辑缺乏强有力的外部业务验收时，AI 存在极大的作弊动机——通过阉割复杂的业务分支、削弱程序原有功能，来换取一段结构更平庸、更容易被机器证明的代码。
| 技术路径 | 核心代表方案 | 适用领域 | 主要优势 | 核心落地短板 |
|---|---|---|---|---|
| 测试升格汇编证明 | Anthropic + Theorem (Claude) | 开源库关键测试桩、C/C++底层模块 | 深入二进制、可自主修补并挖出长尾罕见漏洞 | 缺乏停机保证、证明膨胀严重、绑定单一架构 |
| 轻量级符号执行/检测 | AWS (TLA+ / 自动化推理) | 云计算控制面、访问控制策略 | 工业级成熟、贴合分布式一致性设计 | 需顶级专家建模、无法覆盖复杂实现细节 |
| 纯数学高阶定理证明 | DeepMind (AlphaProof) | 国际奥赛级数学命题、形式化数学库 | 抽象逻辑推理能力极强 | 脱离现实软件工程、难以直接处理系统二进制 |
单桩证明膨胀至 60 万行，也是横亘在维护者面前的现实难题。这些生成的证明中充斥着对寄存器与内存状态的底层死板展开，缺乏高阶数学抽象。这种流水账式的机器证明不仅极其庞大，而且在软件版本迭代时难以维护——上游源码稍作修改，数万行汇编指令位移，整套证明便可能全盘失效，必须重新燃烧 Token 重算。
- 建议.开源库维护者在接收此类 AI 生成的安全证明和源码补丁时，应严查功能退化测试，重点关注异常分支是否因过度简化而被实质性废弃。
这并非否定大模型介入形式化验证的巨大价值。长久以来，工业界在安全防护上一直受制于被动的修修补补；Anthropic 的探索证明了，让大模型以算力暴力抹平极其枯燥的形式化推导，在工程上具有可行性。但当开发者审视这 1.8 亿行机械产物时，应当保有足够的清醒：没有覆盖停机性、不兼容并发、剥离了真实系统调用复杂度的证明，仍是温室里的果实。确定性安全的真正质变，不在于在理想模型里写出多少亿行证明，而在于它何时能承受住真实生产环境无休止的混乱与冲击。