Anthropic 用 Claude 为 123 个开源软件写出 1.8 亿行形式化证明

原创 心兰 2026-10-26 18:24 江苏

↑阅读之前记得关注+星标⭐️，😄，每天才能第一时间接收到更新

人类六十年来建立的软件测试安全感，可能只是一种心理安慰。

即便是被全球最庞大的自动化测试集群轰炸过数万亿次的顶级开源代码，里面依然藏着人类永远测不出来的幽灵漏洞。

Anthropic安全红队刚刚公布了一项颠覆计算机工程的研究。

他们没有用AI去找零星的漏洞，而是让Claude做了一件以往人类想都不敢想的事：

直接给123个主流开源软件、239个程序入口，下达不可推翻的数学判决书。

Claude在编译后的底层机器码（RISC-V汇编）层面，硬生生写出了1.8亿行极其严苛的数学证明。

结论只有一句话：

在小于64MB的任意输入下，这些代码绝对不可能崩溃，绝对不可能发生内存越界，逻辑绝对成立。

这不是概率，这是数学公理。

暴力测试跑几万亿次也只是盲人摸象

现在所有软件公司的防守逻辑全靠测试。

无论是日常的人工测试，还是谷歌OSS-Fuzz这种顶级模糊测试工具，原理都差不多。

算法守在软件门口，生成海量的随机垃圾数据疯狂往里砸，看程序会不会崩。

但真实世界的可能输入是无限的。

哪怕谷歌把全球服务器拉满，跑上几万亿次测试，覆盖的代码路径也只是冰山一角。

Claude在做数学证明的过程中，顺手扒出了大批潜伏十几年的陈年老Bug。

其中一个解压模块的越界写入漏洞极其刁钻：

文件必须恰好在20MB左右，而且内部必须包含一种极其罕见的特定排布格式。

模糊测试工具默认只塞1MB以内的输入，就算让人类的测试服务器跑到宇宙毁灭，也永远撞不进这个特定的死胡同。

还有一个图像解码器的越界读取漏洞，触发门槛是整整64MB的特殊畸形文件加上2GB以上的实时内存消耗。

在暴力穷举面前，这些Bug是隐形的。

但在严密的数学证明面前，只要有一条路径可能导致逻辑破裂，AI的推导就会当场卡死，漏洞无处遁形。

人类一行都不用看，数学负责绝对验票

很多人第一反应是：大模型天天胡说八道，它写的代码谁敢信？

这项研究最精妙的地方，就在于彻底终结了大模型的幻觉原罪。

写出几万行、几十万行的逻辑推导过程，对人类或者AI来说都难如登天。

但是验证推导是否成立，在计算机科学里只需要毫秒级的符号运算。

流程：

开源代码直接编译成底层RISC-V汇编机器码。

Claude在汇编指令里疯狂推演，写出几十万行甚至几百万行的Rocq形式化证明代码。

证明写完，直接扔进完全独立、几十年没有出过差错的Rocq数学检查器。

检查器亮绿灯，证明成立。

检查器报错，说明AI逻辑不通，打回去重写。

这1.8亿行庞大晦涩的证明代码，人类专家连一行都不需要去肉眼复核。

因为负责给代码盖章的是绝对纯粹的数理逻辑。

只要底层的硬件物理模型和操作系统规则没有撒谎，数学检查器一旦放行，就等于给这段代码发了物理意义上的免死金牌。

深入底层机器码的震撼细节

这套验证最让硬核技术人员脊背发凉的，是它深入底层的粗暴程度。

AI根本没有在人类写的高级语言层面打转，它直接在CPU执行的机器码上开刀。

在验证一个网络库cpp-httplib时，为了证明析构函数递归不会撑爆系统栈内存，Claude直接对着机器码做逆向逻辑推演。

在没有任何源码提示的情况下，它硬生生在汇编层证明了libc++内部红黑树平衡旋转算法的最优对数深度。

更夸张的一幕发生在验证Linux内核中的zlib压缩模块。

为了证明这段x86汇编代码百分之百符合RFC 1950国际技术规范，Claude做了一件反客为主的事：

它全自动手搓了一整套x86指令集的形式化数学定义。

这套由AI凭空建立的硬件指令模型，不仅单步调试跑通了Linux内核并成功启动了Ubuntu系统，还反向挑出了芯片官方技术文档里的几百处笔误，甚至抓到了芯片硬件本身的几处缺陷。

在另一个实验里，Claude用Rust写了一个Python解释器，并用Verus工具证明它绝对符合CPython学术规范。

研究人员用170多万个随机生成的Python程序去无差别轰炸实测，这个被数学锁死的解释器，行为一致度达到了99.95%。

面对一款被人类日常翻来覆去审计的成熟PDF阅读器，Claude仅用一周时间，挖出的高危安全漏洞就追平了该软件过去一整年的漏洞公开总量。

昂贵的神器，正在被AI变成白菜价

其实数学证明软件的理论几十年前就有了，但过去几乎没人用得起。

为了证明微内核seL4的绝对安全，人类写代码只用了两年，证明它却花了二十个人年。

以往只有波音空客的飞控系统，或者核电站核心控制模块，才舍得花这种天价去换取零Bug保障。

但大模型彻底改变了这个经济账。

模型越聪明，写出严谨逻辑消耗的Token就越少。

新一代的Opus 5.5在完成相同任务时，消耗的算力比上一代直接暴跌40%。

更关键的是逻辑积木的无限复用。

软件底层的C语言运行时初始化、内存分配、消毒器逻辑，千千万万个程序其实全是一模一样的。

AI智能体接入共享工作区之后，后来的AI直接抄前面AI写完的底层定理。

任务完成成本再度直降17%，通用模块几乎不需要写一行新代码。

就像数学界几百位数学家花了几十年搭建的Lean数学库一样，代码世界底层的数学积木正在被AI以惊人的速度搭成一座摩天大楼。

每一个基础库被AI证明一次，全人类未来就可以永久免费复用这个免死证明。

软件开发的游戏规则彻底变了

当然，现在的系统还谈不上绝对完美。

真实世界的物理芯片可能发生物理扰动，系统环境可能有未被建模的奇异状态，死代码或者调用者的违规乱传参依然可能绕开防御。

但底层的攻守天平已经彻底倾斜。

黑客正在用大模型毫秒级挖掘系统缝隙。

如果防守方还停留在靠人类敲键盘、靠服务器盲目跑测试用例的旧时代，全盘沦陷只是时间问题。

把代码翻译成数学，让AI去穷尽所有维度的逻辑推演，用机器审查机器，给核心软件筑起绝对不可逾越的逻辑防火墙。

那个靠堆算力、拼运气测Bug的旧时代，正在被这场数学风暴撕得粉碎。

source：

https://www.anthropic.com/research/formal-verification

--end--

最后记得⭐️我，每天都在更新：如果觉得文章还不错的话可以点赞转发推荐评论

/...@作者：心兰

跳转微信打开