人类六十年来建立的软件测试安全感，可能仅是一种心理安慰。即便经过全球最庞大自动化测试集群数万亿次轰炸的顶级开源代码，仍潜伏着传统手段无法检测的深层漏洞。
Anthropic安全红队最新公布的一项研究颠覆了计算机工程认知。其并未让AI寻找零星漏洞，而是指令Claude对123个主流开源软件的239个程序入口下达不可推翻的数学判决。Claude在编译后的底层机器码（RISC-V汇编）层面，生成了1.8亿行严苛的数学证明。
结论明确：在小于64MB的任意输入下，这些代码绝对不可能崩溃、发生内存越界或逻辑错误。这不是概率统计，而是基于数学公理的确定性保障。
暴力测试的局限：盲人摸象难寻隐性漏洞
当前软件行业的防御逻辑主要依赖测试，无论是人工测试还是如谷歌OSS-Fuzz等顶级模糊测试工具，其核心原理均为向程序注入海量随机数据以观察是否崩溃。然而，真实世界的输入空间是无限的，即使动用全球服务器进行数万亿次测试，覆盖的代码路径仍是冰山一角。
Claude在进行数学证明过程中，挖掘出大量潜伏十余年的陈旧Bug。例如，某解压模块存在一个极其隐蔽的越界写入漏洞，触发条件需文件恰好为20MB且包含特定罕见排布格式。由于模糊测试通常限制输入在1MB以内，此类漏洞在传统测试中几乎永远无法被触发。另一图像解码器的越界读取漏洞，则需64MB特殊畸形文件及2GB以上实时内存消耗才能触发。
在暴力穷举面前，这些Bug是隐形的；但在严密的数学证明面前，任何可能导致逻辑破裂的路径都会导致推导中断，从而使漏洞无处遁形。
验证机制革新：数理逻辑取代人工复核
针对大模型可能存在幻觉的质疑，该研究构建了闭环验证体系。流程如下：
- 将开源代码编译为底层RISC-V汇编机器码；
- Claude在汇编指令中推演，生成数十万至数百万行的Rocq形式化证明代码；
- 将证明代码投入独立且历经数十年验证的Rocq数学检查器。
若检查器通过，则证明成立；若报错，则AI需重新推导。这1.8亿行证明代码无需人类专家肉眼复核，因为负责“盖章”的是绝对纯粹的数理逻辑。只要底层硬件物理模型和操作系统规则无误，数学检查器的放行即赋予代码物理意义上的安全性保障。
深入底层：从机器码逆向到硬件缺陷挖掘
该验证体系的震撼之处在于其深入底层的粒度。AI未停留在高级语言层面，而是直接对CPU执行的机器码进行逆向逻辑推演。
在验证网络库cpp-httplib时，Claude在无源码提示的情况下，于汇编层证明了libc++内部红黑树平衡旋转算法的最优对数深度，确保析构函数递归不会撑爆系统栈内存。在验证Linux内核zlib压缩模块时，Claude甚至全自动构建了整套x86指令集的形式化数学定义。这套由AI建立的硬件指令模型不仅成功启动Ubuntu系统，还反向纠正了芯片官方技术文档中的数百处笔误，并发现几处芯片硬件缺陷。
此外，在另一项实验中，Claude用Rust编写Python解释器并通过Verus工具证明其符合CPython规范。经170多万个随机生成的Python程序实测，其行为一致度达99.95%。面对一款成熟PDF阅读器，Claude仅用一周时间挖出的高危漏洞数量，便追平了该软件过去一年的公开总量。
成本变革：形式化验证走向普惠
形式化验证理论虽已存在数十年，但因成本高昂，以往仅应用于波音空客飞控或核电站核心模块。例如，证明微内核seL4的安全性强耗二十个人年。大模型的引入彻底改变了这一经济账。
随着模型能力提升，生成严谨逻辑所需的Token消耗大幅降低。新一代Opus 5.5在完成相同任务时，算力消耗较上一代下降40%。更关键的是逻辑积木的复用性：软件底层的C语言运行时初始化、内存分配等逻辑具有高度通用性。AI智能体接入共享工作区后，后续任务可直接复用已验证的底层定理，使通用模块的开发成本降低17%，近乎零代码新增。
正如Lean数学库的积累，代码世界底层的数学证明正被AI快速构建。每个基础库一旦被证明，全人类即可永久免费复用这一“免死金牌”。
结语：软件开发范式的根本性转变
尽管当前系统仍面临物理芯片扰动、环境奇异状态及违规传参等现实挑战，但攻守天平已彻底倾斜。当黑客利用大模型毫秒级挖掘系统缝隙时，防守方若仍依赖传统的人工测试与盲目跑用例，将面临巨大风险。
将代码转化为数学，利用AI穷尽所有维度的逻辑推演，以机器审查机器，为核心软件筑起不可逾越的逻辑防火墙，已成为必然趋势。靠堆算力和运气测试Bug的旧时代，正在这场数学风暴中终结。
source：https://www.anthropic.com/research/formal-verification