报告里说：软件里藏着bug，这事大家都知道。但你知道有多难彻底消灭吗？Linux内核是全球几十亿台设备在跑的系统，维护团队那么多，但就在不久前还有超过1000个安全漏洞被公开披露。以前有一种叫"形式验证"的技术，理论上可以用数学的方式证明代码没有bug。但太费人力了。举个例子，seL4这个操作系统内核，开发花了2年，验证它就花了整整20年。所以这项技术一直只用在飞机这种极端场景下。
后来发生了什么？Anthropic和一家叫Theorem的公司合作，让Claude来做这件事。他们选了谷歌一个叫OSS-Fuzz的项目，里面放着很多开源库的测试用例。结果，Claude在几周内，替123个开源库的239个测试入口点完成了证明，写出来的验证代码有1.8亿行。说白了，这些代码在特定条件下，不管给它输入什么，都不会崩溃。这个结论不是测试出来的，是数学证出来的。
更有意思的是，Claude在证明过程中，还顺带发现了很多之前没人发现的bug。有些bug已经藏了十几年，经历了无数次自动测试都没被抓到。有一个bug需要特定的20MB大小的输入才会触发，普通测试根本不会往那个方向跑。还有一个PDF阅读器，Claude一周内找到的安全漏洞，比这个软件以往一整年被报告的数量还多。
刚开始这套方案成本很高，每个证明需要消耗数亿个token。新版本的Opus 5.5比上一版少用了大约40%。另外，他们发现证明可以复用，就像写代码能调用别人写好的函数一样，上一个证明用过的东西，下一个证明直接拿来用。多个AI同时工作、共享一个工作空间的时候，整体消耗又少了17%。
研究团队也没有夸大结论。他们说"通过形式验证"并不等于"完全没有bug"，因为证明建立在一些假设之上，比如假设程序在特定CPU上单线程运行。现实环境更复杂，这些假设和现实之间的差距，是下一步要填补的地方。
他们的判断是：形式验证这件事，以后会像今天的代码测试一样普及，变成软件开发的标配。
#科技先锋官#