一项利用 Claude AI 智能体进行的自动化安全实验发现，Lean 4 运行时存在堆缓冲区溢出漏洞，该漏洞影响了目前该语言的所有版本。
研究人员 Kiran Anand 利用该 AI 智能体，针对 `lean-zip` 进行了超过 1.05 亿次的模糊测试。`lean-zip` 是 zlib 的原生实现，此前已通过形式化验证，在数学层面被证明是正确的。
尽管经过验证的 `lean-zip` 应用代码未显示任何内存漏洞，但实验却在 Lean 运行时的底层 `lean_alloc_sarray` 函数中发现了一个严重缺陷。
运行时层面的失效
该漏洞发生在分配标量数组（如 `ByteArray`）的过程中。当分配的大小接近 64 位系统的最大可能值时，整数溢出会导致运行时仅分配了一个极小的缓冲区，而系统随后却尝试向其中写入海量数据。
在测试开始前，Anand 剥离了 `lean-zip` 代码库中的所有定理、规范和文档。这种设置确保了 Claude 智能体在不知道代码已通过形式化验证的情况下进行操作，从而避免了算法偏见。
为了定位该漏洞，AI 智能体在包括 ZIP 解压和 gzip 解压缩在内的六个不同攻击面内，同时启动了 16 个并行模糊测试器。该智能体还使用了一系列安全工具，包括 AddressSanitizer、Valgrind 以及多种静态分析引擎。
除了运行时溢出漏洞外，实验还在 `lean-zip` 归档解析器中发现了一个拒绝服务（DoS）漏洞。值得注意的是，该特定组件并未包含在形式化验证流程之内。
目前，相关漏洞报告已提交给 Lean 开发团队，修复程序正在 Lean 4 代码库中等待合并。
