Claude给391行代码找Bug，狂写1.8亿行证明！

　　henry 发自凹非寺

　　量子位 | 公众号 QbitAI

　　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