软件测试能告诉你“跑了多少种输入没有出错”，却很难证明“所有输入都不会出错”。Anthropic 10 月 22 日公布的一项研究，尝试用大模型补上这道缺口：研究团队与 Theorem 合作，让 Claude 在 RISC-V 汇编代码层面为 123 个真实开源库生成形式化证明，并在此过程中发现了多年测试没有抓到的缺陷。
从测试到证明
形式化验证的思路，是把程序和一组安全规则转换成数学模型，再证明程序在所有可能行为下都满足规则。难点在于证明往往比原程序大得多，过去需要高度专业的验证工程师投入数月甚至数年。Anthropic 的做法是把开源项目已有的模糊测试改写成规格：不再只跑有限次随机输入，而是证明在输入小于 64MB、并符合特定 Linux 运行环境模型的前提下，程序不会触发内存安全错误或断言失败。
这套证明针对的是编译后的 RISC-V 汇编，而不是更容易处理的高级语言源码。研究团队称，这是首次大规模把 AI 形式化验证用于生产软件的可执行代码层。Claude 的优势不在于“比人更懂数学”，而在于能持续处理海量代码、失败反例和重复证明工作，把原本需要专家手工推进的搜索过程规模化。
为什么 123 个库值得关注
现代软件依赖大量开源库，任何一个底层组件的内存错误都可能沿着依赖链扩散。研究团队指出，即便是经过海量测试的 Linux 内核，近期也披露了上千个漏洞；当模型越来越擅长把多个小缺陷串成攻击链，仅靠测试和代码审计已经不够。形式化证明的价值，是给出一个比“暂时没发现问题”更强的保证。
这次工作还展示了 AI 在验证过程中的副产品：Claude 在写证明时发现了此前长期未被检测到的 bug。这个结果比“生成了多少行证明”更有意义，因为验证不是形式主义地堆材料，而是迫使系统在边界条件、异常路径和隐含假设上接受检查。Theorem 也开放了同类流水线，并发布帮助开发者上手的 Claude 技能，试图把一次性研究变成可复用工具。
边界仍然很清楚
这项成果不能被解读为“AI 已经证明所有软件都安全”。证明依赖明确假设：程序是单线程静态二进制、使用固定内存预算、运行在特定 RISC-V 处理器和 Linux 环境模型中；证明覆盖的是内存安全和断言等特定属性，不是所有业务逻辑错误。规格本身如果写得不完整，证明也只能保证“符合这份规格”，不能保证“符合真实世界的全部需求”。
成本和工程化同样是门槛。大模型生成证明仍可能失败、走弯路或需要人工修正，验证结果也要由专家审查。更现实的图景是，形式化验证从少数航空、内核项目走向更多基础库，成为 CI 流程中的一道可选防线，而不是替代测试和代码评审。AI 把门槛降下来之后，软件行业需要补的课是规格设计、证据管理和责任归属。证明可以写成机器可检查的形式，但“该证明什么”仍然是人的判断。