AI写代码已经不稀奇了。Anthropic最近公开的一项研究，做的事情更像给代码“验算”：让Claude尝试证明一段程序在特定条件下不会触发某些安全错误。

10月22日，Anthropic的Frontier Red Team发布研究，介绍他们和Theorem合作完成的一组实验。Anthropic称，Claude已经在123个真实开源软件库上尝试证明安全性质，而且验证对象下沉到了RISC-V汇编代码层。

这里的“形式化验证”，和我们平时跑测试不是一回事。

测试是在很多输入下观察程序有没有出错；形式化验证则是先把代码和安全规则变成数学模型，再检查它在设定条件下是否始终遵守这些规则。简单说，测试更接近“这几组情况没出问题”，形式化验证则是在限定范围内证明“只要条件成立，就不能违反这条规则”。

Anthropic给出的例子也有严格前提：程序需要是单线程、静态编译的二进制文件，运行在RISC-V处理器和Linux环境中，内存预算固定，输入小于64MB。满足这些条件时，Claude证明部分程序可以遵守预先设定的安全性质。

所以这条新闻不能简化成“AI已经把软件证明安全了”。

它证明的是某些程序、某些性质和某些运行条件。条件换了，证明范围也要重新计算。

研究中还有一个更容易引起关注的结果：Anthropic称，形式化验证过程中发现了一个潜伏十多年的逻辑漏洞；在检查一款广泛使用的PDF阅读器时，一周发现的安全问题数量，接近这类项目通常一年报告的数量。

不过，这些结果来自Anthropic自己的研究，不等于独立审计，也不代表所有漏洞都已经被找出来。研究样本怎么选、验证规则怎么写、哪些问题被纳入检查，都会影响最终结果。

过去，形式化验证之所以很少进入普通软件项目，不只是因为难，也因为成本高。证明往往比原始代码长很多，需要专门训练过的人逐条处理。模型可以把一部分重复工作接过去，但安全规则怎么定义、证明是否覆盖了真正的风险，仍然需要人来判断。

这项技术也有明显边界。一个证明只能保证它写明的性质，不能顺手证明软件没有其他漏洞。编译器、操作系统、硬件和证明检查器本身，也都在信任范围里。Anthropic在报告的限制部分同样承认，形式化验证有时证明的内容会比我们希望的少。

对普通用户来说，短期内不会突然多出一个“AI安全开关”。更现实的变化是，代码生成越来越便宜以后，安全检查也可能从上线前的补救，提前到开发过程里。

以后一个AI编程工具值不值得用，除了看它写得快不快，也得看它有没有把验证和审计做进去。

（仅属个人观察。）