大多数软件都带着bug运行，而AI已经能较容易地发现甚至利用它们。Anthropic在2026年10月发布的研究博客中提出一个更激进的方向：不再只靠测试和模糊测试找bug，而是用形式化验证证明代码在给定规约下不存在某类bug。他们与Theorem合作，用Claude对123个真实开源库的编译产物（RISC-V汇编）生成形式化证明，这是据其所知首次在汇编代码级别、以AI大规模对生产软件做形式化验证的尝试。

问题：测试永远无法穷尽输入

模糊测试（fuzzing）是当前主流的自动化缺陷发现手段：开发者提供一个入口点，fuzzer不断生成半随机和变异输入，试图让程序崩溃。OSS-Fuzz为符合条件的开源项目提供持续模糊测试，并自动用AddressSanitizer插桩C/C++程序，使非法内存访问触发崩溃。但模糊测试本质是暴力搜索，输入空间无限，无论跑多少次都无法保证覆盖所有代码路径。Linux内核这样经过海量测试的软件仍不断披露漏洞，说明仅靠测试不足以给出安全保证。

形式化验证的思路是：把代码翻译成数学模型，证明它始终满足一组定义好的安全规则；若证明失败，失败的性质会提示bug所在。重复“消除失败原因再证明”的过程，最终可得到“不存在违反该规则的bug”的证明。但传统上证明的规模可达代码的许多倍，且需要高度专业化的技能。seL4内核实现用了两人年，形式化验证却用了20人年，因此过去只有航空电子等关键领域才用得起。

工程链路：把测试变成规约，再让Claude写证明

这项工作的关键工程决策，是绕开“为每个程序手写完整规约”这一最大障碍。对文本编辑器或浏览器，“正确”很难形式化；但对OSS-Fuzz项目，已有大量可编译的测试套件。研究团队把“该测试套件永远通过”编码成规约，并建立在“任意RISC-V编译二进制在Linux上如何执行”的通用模型之上。具体做法是：

  1. 将开源库及其现有fuzz测试编译为RISC-V可执行文件；
  2. 结合Theorem提供的RISC-V指令语义与Linux进程语义，把汇编代码翻译成数学模型；
  3. 将“对任意小于64MB的输入都不崩溃”作为待证性质，与模型一起机械地生成规约；
  4. 由Claude生成Rocq证明，Rocq内核检查证明是否满足规约。

最终，Claude在数周内为123个OSS-Fuzz库的239个入口点修补了发现的bug，并证明了任意小于64MB输入下不会崩溃。证明总量约1.8亿行Rocq，典型证明约60万行，对应二进制的RISC-V指令中位数为1.8万条。证明针对的是编译后的RISC-V指令，而非源代码，因此覆盖了编译器输出这一层。

信任边界：哪些东西仍需人工信任

证明代码量巨大，但几乎不需要人工逐行审查，因为Rocq证明检查器会机械地确认证明满足规约。开发者真正需要信任的只有少数基础件：RISC-V与Linux进程的形式化模型、规约生成逻辑，以及Rocq内核等可信组件。这是形式化验证相对测试的根本优势：测试结果需要人判断覆盖是否充分，而证明的正确性由检查器保证，人的信任面被压缩到模型和工具链。

当前证明的假设也需要明确：程序是单线程静态二进制、内存预算固定、运行在RISC-V CPU的Linux上。这离“修复所有可能的bug”还很远，但研究团队认为扩大范围是可及的，主要工作是标准化更多汇编架构和操作系统进程的语义。

不止于“不崩溃”：其他验证探索

博客还描述了若干初步探索：用其他形式化方法评估zlib压缩算法的安全性、证明Rust编写的Python解释器的行为等价性、以及根除关键软件中长期潜伏的bug。这些方向说明LLM辅助验证不限于内存安全这一种规约，也可用于行为等价、算法安全属性等更丰富的目标。

对企业落地的启示与局限

从工程角度看，这条链路对中国企业的代码审计和供应链安全有几点可操作启示。第一，规约来源可以复用现有测试资产：企业若已有成熟的单元测试或fuzz入口，可优先把“测试永远通过”转成规约，降低形式化的启动成本。第二，验证对象选编译产物而非源码，能覆盖编译器引入的问题，但也要求企业固定目标架构和运行环境语义，否则证明的适用范围会漂移。第三，信任边界要写清楚：模型语义、规约生成器和证明检查器是必须审计的基础件，不能把“AI写了证明”当作安全结论本身。

局限同样明显。当前方法证明的是特定假设下的无崩溃性质，不是功能正确性；多线程、动态内存布局、其他指令集和操作系统尚未覆盖；规约若本身写错，证明再正确也保护不了真正的安全属性。此外，1.8亿行证明的维护成本、模型语义的标准化程度，都是规模化复用的现实约束。Anthropic和Theorem开源了部分证明、RISC-V与OS语义，并发布了一个Claude skill帮助开发者上手，这为评估该方法在自身代码库上的可行性提供了起点。

对AI编程工具链而言，这项工作的意义在于把LLM的长处——在明确定义的目标下处理海量代码——对准了形式化验证这个传统上人力密集的环节。它不意味着形式化验证从此廉价，但确实把“先跑测试、再补证明”变成了一条可以尝试的工程路径。