Claude狂写1.8亿行证明代码，首次实现汇编层大规模形式化验证

Anthropic与Theorem合作开展最新研究，让Claude在几周内为123个开源库中的239个测试入口完成形式化验证，产出约1.8亿行通过机器检查的证明代码。据团队介绍，这是其所知的首次大规模利用AI在汇编代码层面对生产软件开展形式化验证。简单来说，就是让Claude找出Bug、修掉，然后交一份证明，说明规定范围内的这类错误不会再出现。

Claude此次检查的是一批长期接受安全测试、接入谷歌OSS-Fuzz项目的开源库。模糊测试通过给程序喂各种输入来寻找崩溃点，但没试到的地方仍可能藏有Bug。Claude在一个解压器中发现异常：某些输入会让计数器算错，导致程序把数据写到分配好的内存范围之外。触发该错误需要约20MB、内容排列特殊的输入，而以往模糊测试通常将输入限制在1MB以内。团队让Claude证明规定范围内所有输入都不会触发约定错误，尝试证明的过程反过来帮Claude找到了漏洞。据团队介绍，顺着这条思路，Claude已发现数百个Bug，确认后会先修改代码再继续证明。

在cJSON开源库中，一个解析入口只有391行C代码，Claude却交出了约63万行证明。这是因为Claude既要证明这段代码，也得考虑程序调用的基础功能，它还给自己写了工具，自动生成超过一半的证明内容。Claude检查的是编译后的机器指令，团队先为指令和运行环境建立数学模型，再让Claude在模型里证明安全要求。证明完成后交给人类开发的Rocq证明检查器自动验算，只要有一步推理不成立就无法过关。这些证明还能复用，实验中共享证明让同一组任务少用了17%的token。模型升级也在降低消耗：36项小型验证任务中，Opus 5.5完成其中一半所需token比Opus 5少约40%。目前团队已公开25个库、60个测试入口的证明，开发者可下载复用。

研究背后还有一个现实问题：AI也在帮助攻击者提速。10月21日，微软披露攻击组织Storm-0940利用AI代理框架自动攻击全球数百家组织，多个成功案例中从选定目标到拿到云端特权用时不到3小时。Wiz研究团队表示借助AI发现PHP中长期潜伏的漏洞并做出可行利用方式，PHP已于10月21日发布补丁。Cloudflare CEO Matthew Prince披露，漏洞公开后其网络观察到的利用尝试已达数百万次。Anthropic于10月8日推出Cyber Mission支持关键基础设施和开源软件的安全防护，但也承认找到漏洞后确认和修复仍然很难。Anthropic副首席信息安全官Jason Clinton呼吁安全负责人立即向董事会争取支持，先补足基础安全措施，并判断情况在好转前还会恶化，行业可能需要撑过约18个月。