Anthropic 做了一件比“让模型写代码”更进一步的事：让 Claude 为已有代码写出数学证明，证明这些代码确实按预期工作。
发生了什么
据 The Decoder 报道，Anthropic 让 Claude 针对 123 个开源库生成形式化证明代码，总量约 1.8 亿行。这些证明的作用不是运行程序看输出，而是用数学方式论证代码满足其规格。过程中，模型还发现了多年常规测试未能捕获的 bug。Anthropic 给出的目标很明确：让 AI 辅助的形式化验证变得像跑单元测试一样日常。
需要说明的是，报道披露的信息集中在规模与结果层面，具体的证明助手、验证工具链、人工复核比例等工程细节尚未展开，因此对这些数字的解读应保持克制——1.8 亿行证明代码本身不等于 1.8 亿行“有效洞见”，其中大量是可由工具自动生成、机械展开的证明脚本。
为什么重要
形式化验证不是新概念，工业界在高安全领域（芯片、航空航天、操作系统内核）已用了几十年，但它长期是小圈子手艺：写证明的成本往往高于写代码本身，且需要专门的逻辑与证明助手训练。这导致一个尴尬现实——越是关键代码，越难被完整验证。
大模型改变的是成本结构。证明代码高度模板化、依赖大量局部引理和样板结构，恰好落在语言模型擅长的区间。如果生成证明的边际成本大幅下降，形式化验证就可能从“少数专家的一次性工程”变成“开发流程里的常规环节”。这与测试的历史路径相似：测试也曾是专门团队的事，后来成为每个开发者的日常动作。
另一个值得注意的信号是“发现测试漏掉的 bug”。测试只能覆盖想到的输入，证明则试图覆盖所有输入，两者在能力上是互补而非替代关系。
影响与看点
对开发者而言，短期最现实的价值不是自己写证明，而是让模型为关键模块生成验证尝试，把“这段代码为什么对”从口头论证变成可检查的产物。对行业而言，若这条路走通，代码审查、安全审计和合规认证的形态都可能被重塑——审计方要看的或许不再是测试覆盖率，而是证明覆盖了哪些规格。
需要关注的三个点：一是可信度，模型生成的证明若本身有漏洞，会制造虚假安全感，证明检查器必须独立且严格；二是规格从哪来，“证明代码正确”的前提是有人写清楚“正确”是什么，这仍是人的工作；三是可维护性，代码改动后证明需同步更新，否则验证会迅速腐化。
我的判断是：这件事的长期意义大于短期可用性。它真正指向的不是“AI 会写证明了”，而是验证成本下降后，软件质量保障的重心可能从“事后测试”前移到“事前规格与证明”。
