过去48小时，我让一个Claude代理对着号称"数学证明无bug"的代码库跑了1.05亿次模糊测试。结果它真找到了漏洞——在一段被Lean定理证明器验证为"完全正确"的压缩库实现里。
这事得从Anthropic最近的一个决定说起。他们搞了个叫Mythos的AI代理，专门挖软件漏洞，结果发现这东西太能找了，干脆选择不发布，理由是"太危险"。不管这是不是营销话术，有个趋势已经很明显：发现安全漏洞的成本正在崩盘式下跌，而市面上绝大多数软件当初设计时就没想过要扛住这种级别的 scrutiny（审查）。
软件危机在敲门。于是"形式化验证"成了新救命稻草——用机械工具给代码做数学证明，能不能造出真正刀枪不入的软件？
10个AI代理，3个月，造了个"数学担保"的压缩库
Lean生态最近交了一份答卷。10个自主代理花了3个月，从零构建并证明了zlib的一个完整实现，叫lean-zip。Leo De Moura，Lean FRO的首席架构师，发了张AI生成的庆祝图（对，他就好这口），核心信息很明确：这不是又一个zlib山寨版，而是一个被Lean端到端验证为正确的实现——Lean保证它完全没有实现层面的bug。
验证长什么样？核心定理之一长这样：
theorem zlib_decompressSingle_compress (data : ByteArray) (level : UInt8) (hsize : data.size < 1024 * 1024 * 1024) : ZlibDecode.decompressSingle (ZlibEncode.compress data level) = .ok data
翻译成人话：任何小于1GB的字节数组，先压缩再解压，结果跟原来一模一样。压缩和解压是完全互逆的。这对函数被证明"完全正确"。
听起来很美好。但我好奇一件事：证明器的保证，到底能管多宽的范围？
我的测试设置：故意"骗过"AI代理
周末我做了个实验。把lean-zip代码库精简了一下，扔给Claude代理，配上AFL++、AddressSanitizer、Valgrind和UBSan这套模糊测试全家桶。
关键操作有三步：第一，删掉所有定理和规格说明；第二，扔掉所有markdown文档；第三，剔除lean-zip里作为备选方案的C FFI绑定。剩下的只有"被验证过的代码本身"——原生的Lean DEFLATE、gzip、ZIP归档和tar实现。
为什么要这么干？我怕Claude知道这是"无bug代码"就提前放弃。蒙住它的眼睛，让它像对待普通代码一样干活。
105,447,392次执行后，代理报了一个问题。
找到的bug：验证覆盖了代码，但没覆盖到"代码怎么跑起来"
漏洞出在lean-zip的C FFI绑定层——没错，就是我故意剔除的那部分。但等等，我明明把C FFI从测试代码里删了，代理怎么找到的？
代理在分析原生Lean代码时，发现了一处内存管理假设。Lean的runtime（运行时）和C代码交换数据时，有个指针生命周期的问题。定理证明了"压缩函数数学上正确"，但没说"当C代码调用这个函数时，指针会不会提前被垃圾回收"。
具体来说，lean-zip的C FFI在把Lean ByteArray传给C库时，没有正确注册GC root（垃圾回收根）。如果C代码执行期间触发了Lean的GC，那块内存可能被挪走或释放。数学上数据是对的，物理上内存可能已经没了。
这个bug在纯Lean环境里永远不会触发——Lean的runtime保证内部调用安全。但只要有人用C FFI调用lean-zip，特定压力下就会崩溃。
讽刺的是，Leo De Moura的官宣推文里特别强调了"端到端验证"。技术上没错，但验证的边界停在Lean代码层面，没延伸到"Lean代码如何被外部世界调用"。C FFI是lean-zip项目的一部分，却不在定理的射程内。
形式化验证的盲区：接口即漏洞
这不是lean-zip的特例。看整个形式化验证领域，有个反复出现的模式：你证明了A，但系统真正运行的是A+B+C+D，而BCD全是信任假设。
CompCert（验证过的C编译器）花了十几年处理这个问题。他们证明"编译器前端到汇编的转换正确"，但预处理、汇编器、链接器、运行时库全在信任边界外。2015年有人发现CompCert的汇编器后端有个bug——不是编译器核心错了，是汇编器优化pass（遍）没进验证范围。
seL4微内核更极端。7000行C代码被证明功能正确，但证明假设"硬件按手册工作"。2014年ARM Cortex-A9的 errata（勘误表）曝光，有些CPU行为跟手册不一样，seL4的假设在特定芯片上失效。
lean-zip的C FFI问题属于同一类：验证的是"函数数学行为"，假设的是"运行时环境行为"。当C代码跨过语言边界时，GC策略、内存布局、调用约定全成了未验证的信任根基。
代理找到的bug，本质是验证边界和实际攻击面的错位。定理覆盖的代码没问题，但代码的"接口皮肤"是漏的。
AI代理的价值：它不懂数学，但会"蛮干"
这里有个有趣的对比。形式化验证是"构造性"的——人写规格，人写证明，系统检查证明是否成立。整个过程是自上而下的，依赖人对"什么需要验证"的判断。
AI代理的模糊测试是"破坏性"的——它不懂DEFLATE算法，不知道你在证明什么，只是疯狂喂输入、观察是否崩溃。自下而上，不依赖人的边界判断。
我的Claude代理在105 million次执行里，构造出了触发GC压力的特殊输入序列。它不知道GC root是什么，只是发现"某种调用模式下程序会segfault（段错误）"。
这种"蛮干"恰好补上了形式化验证的盲区。验证保证"内部无错"，但接口层面的假设需要外部检验。AI代理的成本 collapse（崩塌）意味着这种检验可以规模化、常态化。
Leo De Moura在推文中说lean-zip是"AI辅助形式化验证"的里程碑。我的实验说明另一件事：AI辅助的漏洞发现，同样能突破形式化验证的防线——不是证明错了，是证明的范围被人为限制了。
行业启示：验证不是终点，是起点
这事对软件行业有什么意义？
首先，别神化形式化验证。它是极强的工具，但工具总有边界。lean-zip的C FFI bug说明，验证的规格本身可能就是攻击面。当你说"已验证"时，最好说清楚"验证了什么、假设了什么"。
其次，AI代理的漏洞发现能力正在改变游戏规则。Anthropic不敢放Mythos，不是怕它太弱，是怕它太强。当发现漏洞的成本趋近于零，存量软件的技术债会被集中追偿。形式化验证是应对策略之一，但不是万能药。
最后，组合可能是答案。形式化验证保证核心逻辑，AI代理持续 fuzz（模糊测试）接口和集成点，人用代码审查填补两者的缝隙。lean-zip项目本身就在做这个——10个代理写证明，同时代码开源接受 scrutiny。
我的实验之后，把发现报给了Lean FRO。Leo的回复很直接：「C FFI层确实不在验证范围内，这是个已知限制。我们会加强文档说明，并考虑用更严格的FFI模式。」
没有否认，没有辩解。这种态度在形式化验证圈子里其实挺常见——证明的价值不在于"无错"的幻觉，而在于精确知道"什么被保证了、什么没有"。
105 million次测试找到一个边界案例。这个案例本身不难修，加几个GC root注册就行。但它揭示的问题会持续存在：软件系统的验证边界，和实际运行时的攻击边界， rarely（很少）完全重合。
当AI代理让漏洞发现变得廉价，这种错位会被不断曝光。形式化验证社区需要习惯一件事——你的证明会被机器用你想象不到的方式挑战。这不是威胁，是进化压力。
lean-zip依然是了不起的成就。10个代理3个月造出工业级压缩库，附带数学正确性保证，这在五年前不可想象。但我的周末实验也说明，"数学正确"和"生产安全"之间还有路要走。
热门跟贴