本文作者 Leonardo de Moura 是 Lean 证明助手的创造者，微软研究院Principal Researcher。他深入论述了 AI 生成代码时代为什么必须形式化验证，以及未来验证平台需要什么。

🚨 核心问题：AI 正在重写世界，但没人验证

• Google 和 Microsoft 报告 25-30% 的新代码由 AI 生成
• AWS 用 AI 重写了 4000 万行 COBOL 代码
• Microsoft CTO 预测：2030 年 95% 的代码将由 AI 生成
• Anthropic 用并行 AI Agent 两周构建了 10 万行 C 编译器

📊 现状：测试 ≠ 证明

测试提供的是信心，证明提供的是保证。区别很大。

"Testing provides confidence. Proof provides a guarantee."

一个经典例子：

AI 重写了 TLS 库，代码通过所有测试。但规范要求恒定时间执行——不能有分支依赖于密钥位，不能有内存访问模式泄露信息。AI 的实现包含一个微妙的条件分支，会产生时序侧信道攻击。这个漏洞在测试和代码审查中都看不见，但形式化证明能立即发现。

🛠️ 验证平台的必要条件

1. 小而可信的内核

• 几千行代码的内核，检查每一步证明
• AI 和自动化都在信任边界之外
• 独立重实现作为交叉验证

2. 分离的验证层

• 验证层必须与生成代码的 AI 分离
• 如果同一厂商提供 AI 和验证，存在利益冲突
• 独立验证是安全架构要求

3. 编程语言 + 定理证明器

• 代码和证明在同一系统，无翻译gap
• 丰富的可扩展 tactic 框架
• AI 必须控制证明搜索，而不是委托给黑盒

4. 最大的形式化知识库

• Mathlib：超过 200,000 条形式化定理
• 5 位 Fields 奖得主参与 Lean
• 数学家和工程师使用同一平台

🔥 AI 社区的选择：Lean

💡 核心洞察

"The friction of writing code manually used to force careful design. AI removes that friction, including the beneficial friction. The answer is not to slow AI down. It is to replace human friction with mathematical friction."

手写代码的有害摩擦被 AI 消除了，包括那些有益的摩擦。答案不是放慢 AI，而是用数学摩擦替代人类摩擦：让 AI 快速行动，但让它证明自己的工作。

🌟 结论：验证不是成本，是催化剂

当 AI 能像生成未验证代码一样容易地生成验证代码时，验证不再是成本，而是催化剂。

• ML 内核优化：测试和认证从数月缩短到数小时
• 硬件验证：从一年缩短到数周
• 安全关键系统：认证时间大幅压缩

验证、测试和规范一直是瓶颈，不是实现。好的工程师知道他们想构建什么，只是负担不起证明它。如果成本降到接近零，每个正确性重要的领域都会加速。