「测试通过」和「永不崩溃」差多远
软件测试的本质是抽样：跑一万个输入没崩，第十万零一个照样可能崩。所以行业里一直有另一条路叫形式化验证（formal verification，把代码翻译成数学模型，再证明它永远满足某条规则）。它的地位很高，代价也很高——官方文章给了一个对比：seL4 那个操作系统内核，写代码用了 2 人年，做形式化验证用了 20 人年。
10 月 22 日，Anthropic 发布了一篇研究：和 Theorem（一家做验证工具的公司）合作，用 Claude 在汇编代码层面给 123 个真实开源库证明了安全属性。按他们的说法，这是首次在汇编层对生产软件做大规模型形式化验证。
具体证了什么
证明的命题不抽象：在「输入小于 64MB」的前提下，这些程序在任意输入、任意被建模的 Linux 系统响应与内存布局下，总是正常退出，不会踩内存、不会断言失败。前提条件写得很诚实——被测程序得是单线程静态二进制、内存预算固定、跑在 RISC-V 芯片的 Linux 上。
做法也不是从零写规格。他们挑的是 Google OSS-Fuzz 那批项目里已有的模糊测试（fuzzing，用海量随机变异输入去撞崩溃）入口，把它编译成 RISC-V 可执行文件，再把「这套测试永远不崩」这条规则本身变成数学规格。剩下的活交给 Claude 写证明，写完由 Rocq 检查器机械校验——人不用信 Claude，信检查器就行。
副产品很有意思：为了让证明成立，Claude 得先自己生成 RISC-V 指令集和操作系统的形式语义；这份语义不仅能让 Ubuntu 用户态单步跑起来，生成过程中还揪出了官方参考文档里数百处错误，以及少量硬件本身的缺陷。
成本被砍掉之后，发生什么
过去形式化验证只在航电、内核这类「出错会死人」的地方用得起，因为写证明的人少、证明比代码长好几倍。现在文章给出的判断是：写证明的成本随模型能力下降，且证明可复用、可改造，规模越大越摊得薄。
更值钱的是它顺手抓到的 bug。这些库被 fuzz 跑了上万亿次，Claude 在写证明的过程中还是找出了藏了好几年的问题——因为模糊测试只能撞到「跑得到」的路径，证明要覆盖「所有」路径。两类手段的差别，就在这句话里。
两个必须自己说清的限制
第一，它没修好所有 bug。证明的是「不崩、不踩内存、断言不失败」这一层，业务逻辑对不对、会不会算错钱，证明不管。文章自己写了：离修好全部问题还很远。
第二，奖励作弊的风险是真的。模型完全可以把程序改成「永远不崩」，然后轻松证明——这在学术上叫 reward hacking（钻评分规则的空子）。他们的应对是惩罚任何代码补丁、只奖励「证明清楚改了哪些输入、改动多小」，并且人工审计补丁。
另外，信任链也有前提：你得信 Rocq 检查器、信编译器、信硬件、信那套语义模型没写错。
能不能自己用
可以。部分证明（theorem-labs/oss-verify-proofs）和那套 RISC-V 与 Linux 进程语义都已开源；Theorem 还放了一个 Claude 技能包，教开发者给自己的项目起验证。
对做企业数字化/小团队的实际启发
第一，短期内别指望给客户的业务系统做全量证明。真正能落地的是关键环节：解析文件的那段代码、处理金额的那段代码、对外暴露的接口。挑三个点，比全面铺开有用。
第二，这件事重新定义了「测试覆盖率」的价值。覆盖率告诉你哪些代码被跑过，证明告诉你哪些路径不可能出错。给客户写验收标准时，可以把「关键模块有形式化规格」列为加分项，哪怕只是把输入约束写清楚。
第三，AI 写代码之后，审代码的方式必须升级。模型能批量产出代码，也能批量找漏洞；当找漏洞变得便宜，唯一还贵的防线就是「证明它对」。这个判断，值得写进你给客户的架构建议里。
评论交流
欢迎留下你的想法