Claude给391行代码找Bug，狂写1.8亿行证明！首次大规模汇编层形式化验证

Claude这家伙，也是把debug，玩成扫雷硬解了。

就在刚刚，Anthropic发布了与Theorem合作的最新研究：

让Claude在几周内，为123个开源库中的239个测试入口完成形式化验证，最终产出约1.8亿行通过机器检查的证明代码。

据A社（全美班）团队介绍，这是其所知的首次大规模利用AI，在汇编代码层面对生产软件开展形式化验证。

听起来有点绕，但简单来说，其实就是让Claude找出Bug，修掉，然后交一份证明，说明规定范围内的这类错误不会再出现。

这就像在软件里扫雷，扫完还得写份报告，交代清楚：为什么这里没雷？

而为了写出这份证明，Claude还真挖出了一批藏得很深的Bug。

测试没撞上的Bug，被证明揪出来了

具体来说，Claude这次检查的，是一批长期接受安全测试的开源库。

这些库接入了谷歌的OSS-Fuzz项目。测试工具会给程序喂各种输入，看看哪一种能把它搞崩，再顺着崩溃的地方找Bug。这种方法，就叫“模糊测试”。

比如，正常用户上传一张完整图片，测试工具偏要反着来：把文件截掉一半，改几个字节，看看程序还能不能接住。

试得越多，就越有机会撞上问题，但没试到的地方，仍然可能藏着Bug，就像下面这样：

但你别说，试着试着，还真让Claude在一个解压器里发现了异常：某些输入会让计数器算错，导致程序把数据写到分配好的内存范围之外。

要触发这个错误，你得喂进去一份大约20MB、而且内容排列非常特殊的输入，类似于卡bug。

以往的模糊测试通常把输入限制在1MB以内，如果你按这个限制继续测，自然碰不到那份20MB的数据。

那为啥Claude就发现了呢？是因为团队给它换了一道题：证明规定范围内的所有输入，都不会触发约定的错误。

也就是说，这份20MB的数据也在Claude扫射的范围内。

只要它还能让程序出错，那份“不会出错”的证明就无法成立。于是，尝试证明的过程，反过来帮Claude找到了漏洞。

据团队介绍，顺着这条思路，Claude已经发现了数百个Bug。确认问题后，Claude会先修改代码，再继续证明修改后的程序。

391行代码，交了63万行“解题过程”

那么，为了完成这些证明，Claude写了多少东西？

有一说一，这可能是新的tokenmaxxing赛道：在一个叫cJSON的开源库里，一个解析入口只有391行C代码，Claude却交出了约63万行证明。

之所以这么烧token，是因为Claude既要证明这段代码，也得考虑程序调用的基础功能。

具体的，为了处理大量重复工作，Claude还给自己写了工具，自动生成了超过一半的证明内容。

而且，它检查的是编译后的机器指令，也就是程序交给处理器执行的那个版本。团队还得先为指令和运行环境建立数学模型，再让Claude在模型里证明安全要求。

最后，Claude写完证明，还要交给人类开发的Rocq证明检查器。

具体流程是这样的：

Rocq会按照逻辑规则自动验算。只要有一步推理不成立，这份证明就过不了关。

视频详情

换句话说，Claude这招写证明Debug的思路，跟AI做数学题还挺像，机器也能自动验算，但要推广到更多软件，仍需要人类把关。

不过，好消息是这些证明还能复用。不同程序经常共用基础功能，Agent可以借用、修改已有证明，不必每次从头写。实验中，共享证明让同一组任务少用了17%的token。

与此同时，模型升级也在降低消耗：在36项小型验证任务中，Opus 5.5完成其中一半所需的token，比Opus 5少了约40%。目前，团队已公开25个库、60个测试入口的证明，开发者可以下载复用。

另一边，安全圈已经急了

说到这，这项研究背后还有一个现实问题：AI也在帮助攻击者提速。

10月21日，微软披露，攻击组织Storm-0940利用AI代理框架，自动攻击全球数百家组织。多数目标没有被成功攻破，但在多个成功案例中，攻击者从选定目标到拿到云端特权，用时不到3小时。

最近披露的PHP2Shell，同样让安全圈捏了把汗。

PHP是WordPress等大量网站依赖的底层技术。Wiz研究团队表示，他们借助AI发现了其中长期潜伏的漏洞，还做出了可行的利用方式，可能让攻击者无需登录，就能在受影响的服务器上执行代码。PHP已于10月21日发布补丁。

不过，补丁发出来，还得各个网站及时装上。与此同时，攻击尝试已经迅速增加。Cloudflare CEO Matthew Prince披露，漏洞公开后，其网络观察到的利用尝试已达数百万次。至于其中有多少使用了AI，目前还不清楚。

可以说，防守这块能不能跟上，已经成了眼前的问题。

A社也在10月8日推出Cyber Mission，支持关键基础设施和开源软件的安全防护。

不过，它自己也承认：找到漏洞之后，确认和修复仍然很难。尤其是电网、水务、工厂里的设备，总不能来一句“更新已完成，请立即重启”。

围绕近期接连披露的攻击，网友Chubby，判断眼下可能正在迎来一个转折点。

在转发Anthropic副首席信息安全官Jason Clinton的警告时，他表示，自己向来不是末日论者，但当前局势确实显得严峻。

Clinton则呼吁安全负责人立即向董事会争取支持，先补足基础安全措施。

他个人判断，情况在好转前还会恶化，行业可能需要撑过约18个月。

而Claude这次尝试再往前走一步：改完代码，还得交出一份“为什么这样就安全了”的证明。

参考链接[1]https://www.anthropic.com/research/formal-verification

文章来自于微信公众号 “量子位”，作者 “量子位”