Lean 创始人：当 AI 开始写代码，谁来证明它是正确的？

本文永久链接 – https://tonybai.com/2026/11/07/when-ai-writes-code-who-proves-it-works

大家好，我是Tony Bai。

【导读】

AI 已经能够写出越来越复杂的代码，甚至可以自主调试、重构和提交 PR。

但有一个问题始终没有消失：我们如何证明 AI 写出的代码真的正确？

在 The Data Exchange 的一次专访中，Lean 创始人 Leo de Moura 提出了一个值得软件工程师认真思考的观点：AI 不仅正在改变代码生成，也正在让形式化验证变得前所未有地可行。

从 Lean、自动形式化，到 AI 生成机器可检查的证明，再到未来的 Verified Software Stack，一场围绕软件正确性的技术变革，可能才刚刚开始。

【文章要点】

1. 测试无法证明没有 Bug。测试能够发现错误，但形式化验证可以针对明确的规格说明证明程序性质，对所有满足前提的输入成立。
2. AI 正在降低形式化验证的成本。大模型已经能够将程序转换为 Lean 模型，并生成机器可检查的证明。
3. 规格说明将成为软件工程的核心资产。当代码可以被 AI 重写，真正需要长期维护的是需求、性质、模型和架构约束。
4. 形式化验证将进入 Agent 安全领域。沙箱、权限策略以及 Agent 的行为约束，都需要可信的实现。
5. 程序员的价值将向更高抽象层迁移。定义问题、编写规格、设计系统和判断证明是否覆盖真实需求，将变得更加重要。

想象一下这样一个未来：

你不再需要亲自编写 Go、Rust 或 C 代码，只需要告诉 AI 你希望软件具备什么性质。AI 负责生成实现、编写测试、修复 Bug，甚至完成性能优化。

每次修改完成后，它还会附上一份机器能够检查的数学证明，证明新版本依然满足原来的要求。

这听起来像是科幻小说，但它正在逐渐成为现实。

过去，软件工程师最重要的能力之一是编写正确的代码。后来，测试驱动开发、静态分析、代码审查和持续集成逐渐建立起一套质量保障体系。

而现在，AI 正在让代码生成变得越来越容易。

一个新的问题也随之出现：

如果 AI 可以在几分钟内生成数千行代码，我们如何确定这些代码没有隐藏的错误？

2026 年 10 月，The Data Exchange 发布了一期非常值得软件工程师关注的专访。主持人 Ben Lorica 的对话对象，是 Lean 创始人、AWS 杰出科学家 Leo de Moura。

这次对话的主题非常直接：

When AI Writes the Code, Who Proves It Works?

当 AI 开始写代码，谁来证明它真的有效？

Leo de Moura 给出的答案，指向了一个过去相对小众、如今可能迎来重大转折的技术领域：形式化验证（Formal Verification）。

代码生成已经不再是最大的难题

先看一个现实。

今天，Claude Code 等 AI 编程 Agent 已经可以完成相当复杂的开发任务。它们能够阅读代码库、理解调用关系、修改多个文件、运行测试，甚至自主提交 Pull Request。

但是，测试通过真的意味着程序正确吗？

显然不是。

传统软件开发通常采用这样的质量保障方式：

• 编写代码，实现业务需求。
• 编写单元测试和集成测试。
• 通过代码审查和静态分析发现潜在问题。
• 在 CI 流水线中执行测试，确保修改没有破坏已有功能。

这套体系非常重要，但它有一个天然的局限性：测试只能验证被执行到的场景。

即使你编写了数万个测试用例，也无法穷举所有可能的输入、状态和执行路径。

Leo 在专访中用了一句话概括两者的区别：

Testing is great for showing the presence of bugs, but not their absence.

测试擅长证明 Bug 存在，却无法证明 Bug 不存在。

这句话值得反复琢磨。

假设我们实现了一个数据压缩库，测试覆盖了大量输入，所有测试都通过了。

但我们真正想要保证的性质是什么？

无论输入数据是什么，无论采用什么合法压缩参数，只要压缩成功，再解压缩，就必须恢复原始数据。

这不是一个简单的测试用例，而是一个需要对所有合法输入成立的性质。

形式化验证正是为此而生。

形式化验证究竟是什么？

形式化验证的核心思想，是使用数学语言描述程序应该满足的性质，然后通过数学证明，让机器检查程序是否满足这些性质。

这里需要引入三个概念：

• Specification（规格说明）：程序应该满足什么性质。
• Implementation（实现）：实际运行的程序。
• Proof（证明）：实现满足规格说明的机器可检查证据。

例如，一个整数排序函数，我们希望它满足两个性质：

1. 输出序列是有序的。
2. 输出序列与输入序列包含完全相同的元素。

我们可以用 Lean 描述这样的性质：

def IsSorted (xs : List Nat) : Prop :=
  xs.Pairwise (· ≤ ·)

def SameElements (xs ys : List Nat) : Prop :=
  ∀ x, x ∈ xs ↔ x ∈ ys

这里，Prop 表示一个逻辑命题。

我们不是简单地告诉 AI：“请帮我写一个排序函数”。

而是告诉它：

“请实现一个排序函数，并提供机器可以检查的证明，证明排序结果有序，而且没有丢失或增加任何元素。”

Lean 会检查证明是否成立。

Lean 最重要的设计之一，是将信任边界集中在一个相对精简的证明检查内核（Kernel）上。

开发过程中可以使用 AI、代码生成器、自动补全和各种复杂工具，但最终的证明仍然需要通过内核检查。

换句话说，AI 可以负责寻找证明，Lean Kernel 则负责检查证明。

这带来了一种不同于传统软件测试的信任机制。

AI 正在让形式化验证迎来自己的 ImageNet 时刻

如果形式化验证如此强大，为什么过去没有成为软件开发的主流？

Leo 的回答很简单：太贵了。

过去，形式化验证往往需要开发人员具备较深的数学基础和专门的证明助手知识。

不仅要实现程序，还要构建数学模型、定义性质，再手工完成证明。

对于绝大多数商业软件来说，这样的投入并不现实。

但大模型正在改变这个成本结构。

Leo 在专访中提到了一个非常关键的概念：Autoformalization（自动形式化）。

所谓自动形式化，就是让 AI 将自然语言描述、数学论文，甚至已有程序，转换成 Lean 能够理解的形式化模型。

过去，研究人员需要花费大量时间手工完成这项工作。

现在，前沿模型已经能够在很大程度上自动完成它。

这意味着形式化验证的入口正在发生变化。

AI 不仅能写代码，还能写证明

专访中有一个非常有代表性的案例。

Lean 社区研究者 Kim Morrison 曾尝试使用 Lean 实现 zlib 压缩库，并为其定义了一个关键性质：

对于成功压缩的数据，解压缩之后必须能够恢复原始数据。

这不是简单地运行几个测试用例，而是通过数学命题描述压缩与解压缩之间应该满足的关系。

如果 AI 能够同时生成实现和证明，那么开发人员就不必完全依赖人工编写复杂的验证代码。

Leo 认为，AI 现在已经能够完成相当多这样的工作。

更有意思的是，他还提到了一个 Rust 领域的实践。

微软的密码学团队 SymCrypt 使用 Aeneas 和 Lean 验证密码学代码。

Aeneas 是一套能够将 Rust 程序转换为适合形式化推理的表示形式的工具。

这意味着，即使你的项目不是用 Lean 编写的，也不一定需要把整个项目迁移到 Lean。

更进一步，AI 还可以直接阅读已有代码，尝试构建对应的 Lean 模型。

这种能力在过去一年中取得的进展，让 Leo 自己都感到意外。

Claude Code 已经开始用 Lean 检查自己

专访中还有一个特别值得关注的案例。

Leo 提到了 Claude Code 的核心开发者 Boris 在一次实验中，让 Claude 检查 Claude Code 自身的 Bug。

整个过程相当有意思：

1. Claude 阅读 Claude Code 的源代码。
2. 尝试构建对应的 Lean 模型。
3. 针对关键性质生成形式化证明。
4. 在证明无法成立时，进一步调查代码问题。
5. 发现真实 Bug，并提交修复 PR。

最终，Boris 审查并合并了这些 PR。

Leo 特别提到，Boris 当时甚至并不了解 Lean。

这说明 AI 正在降低形式化验证的使用门槛：开发人员可以先通过 AI 获得实际价值，再逐步学习如何阅读模型、理解性质和检查证明。

不过，这里有一个必须强调的技术细节：

证明一个模型正确，不等于证明原始程序正确。

AI 根据源代码生成 Lean 模型时，可能错误地理解原始程序。

例如，原始程序存在一个整数溢出问题，但 AI 建立的模型却忽略了机器整数的位宽限制，那么 Lean 完全可能证明这个模型正确，而原始程序仍然存在 Bug。

因此，Leo 特别强调了模型忠实性（Faithfulness）问题。

一个重要的解决方向是 Differential Testing：让原始程序和 Lean 模型使用相同输入，比较两者的实际行为，寻找不一致之处。

而在 Rust 等语言中，还可以借助 Aeneas 等工具，进一步建立源代码与形式化模型之间的联系。

这也是为什么不能简单地把“AI 生成了 Lean 证明”等同于“软件已经没有 Bug”。

真正可靠的验证，需要同时关注规格说明、模型与实际实现之间的对应关系。

Mathlib：AI 时代的数学基础设施

如果说 AI 自动生成 Lean 证明是一个技术突破，那么 Mathlib 的存在（Lean 生态中的大型形式化数学库），则让这个突破具备了规模化的可能。

Mathlib 是 Lean 社区长期建设的形式化数学基础设施。

根据 Leo 在专访中的介绍，Mathlib 已经积累了约 250 万行代码。

这意味着大量数学定义、定理和证明已经被转化成机器可以理解和检查的形式。

更令人惊讶的是，AI 正在把这个过程的速度提升到一个新的量级。

Leo 在访谈中提到，AI 生成的部分 Lean 证明已经达到数千万行规模，并以 Anthropic 生成的费马大定理形式化证明为例。

这里的重点并不是代码行数本身，而是 AI 开始能够大规模填充过去需要数学专家花费多年时间完成的形式化证明工作。

Mathlib 原本是人类数学家长期积累的成果，现在它正在成为 AI 进行数学推理和证明的基础设施。

而这种模式显然不只适用于数学。

未来最重要的代码，可能是规格说明

这可能是整场专访中，对软件工程师影响最大的一部分。

当 AI 能够生成代码、测试，甚至形式化证明时，工程师的核心工作究竟是什么？

Leo 和主持人 Ben Lorica 讨论了两个重要概念：

• Requirement Gap：需求鸿沟。
• Model Gap：模型鸿沟。

Requirement Gap，指的是用户真正想要的东西，与我们能够准确写下来的规格说明之间的差距。

比如，产品经理说：“我要一个安全、可靠、高性能的支付系统。”

这句话显然无法直接变成可以证明的数学性质。

什么叫安全？什么叫可靠？性能指标是多少？在网络分区、数据库故障和并发请求下，系统又应该如何表现？

这些问题都需要进一步精确化。

Model Gap，则是规格说明和真实运行环境之间的差距。

即使你写出了严谨的数学模型，也必须考虑它是否真实反映了生产环境。

例如：

• 是否考虑了网络延迟和丢包？
• 是否考虑了并发竞争和资源耗尽？
• 是否考虑了攻击者可以主动构造输入？
• 是否考虑了数据库故障和进程崩溃？

一个模型可以在数学上完全正确，但如果它遗漏了真实世界中的关键条件，那么证明的实际价值就会受到限制。

这也意味着，形式化验证不能取代系统设计和工程判断。

从代码仓库到规格说明仓库

Leo 提出了一个非常有启发性的设想：

过去，软件团队通常维护代码、设计文档和架构图。

但这些文档与实际实现之间，往往没有可靠的自动化对应关系。

代码修改了，文档可能没有更新。

文档修改了，也没有工具能够自动确认代码是否仍然符合设计。

而未来，如果规格说明能够被形式化，并与实现建立可检查的关系，情况就会发生变化。

传统软件开发模式：

需求文档 / 架构设计 -> 人工编写代码 -> 测试 / Code Review / CI

文档与代码之间主要依赖人工维护一致性。

而 AI + 形式化验证模式：

形式化规格说明（Specification） -> AI 生成实现与证明 -> 机器检查 / 测试 / 模型一致性验证

规格说明成为持续演进、可以检查的工程资产。

这带来了一个值得思考的变化：

如果 AI 可以随时根据需求重新生成实现，那么我们为什么一定要把原来的代码视为最重要的资产？

也许真正值得长期维护的，是规格说明、系统模型、架构约束和已经验证过的性质。

代码可以被重写，但系统应该满足什么要求，不能每次都从头猜测。

这并不意味着代码不再重要，而是代码的角色可能从核心知识载体，逐渐转变为规格说明的一种可生成实现。

Verified Software Stack：从验证程序到验证整个软件栈

Leo 在访谈中提出了一个非常重要的概念：Verified Software Stack（经过验证的软件栈）。

他的意思是，不是所有软件都需要投入同样的形式化验证成本。

一个视频游戏存在 Bug，可能只是影响用户体验。

但如果操作系统、编译器、网络通信层或者 TCP/IP 协议栈存在严重缺陷，后果可能完全不同。

这些基础设施构成了现代计算系统的关键软件栈。

如果我们能够为这些组件建立精确的规格说明，并逐步证明实际实现符合规格，那么软件系统的可信度将得到根本性提升。

我认为，这个方向与 AI Agent 的发展尤其相关。

AI Agent 的安全边界，也需要被证明

今天，越来越多的 AI Agent 已经可以执行真实操作：

• 访问文件系统。
• 执行 Shell 命令。
• 调用外部 API。
• 修改代码和配置。
• 操作云资源。
• 自主运行数小时甚至数天。

为了控制这些 Agent，我们通常会采用 Sandbox、权限控制和安全策略。

但这里有一个容易被忽略的问题：

如果负责执行安全策略的代码本身存在 Bug，那么策略写得再完善，也没有意义。

例如，你规定 Agent 只能访问某个工作目录。

但如果沙箱存在路径穿越漏洞，Agent 仍然可能访问目录之外的文件。

又或者，你定义了非常严格的权限策略，但权限检查代码存在并发竞争问题，导致 Agent 绕过限制。

Leo 认为，Agent 的安全边界本身也应该成为 Verified Software Stack 的一部分。

这意味着未来可能需要形式化验证：

1. Sandbox 的隔离性质。
2. 权限检查与策略执行逻辑。
3. Agent 之间的通信协议。
4. 工具调用的授权边界。
5. 长时间运行 Agent 的关键状态转换。

这里还有一个更深层的信任问题。

如果让一个 AI Agent 负责生成证明，那么我们如何确保它没有利用证明系统自身的漏洞？

Leo 提到，Lean 生态正在发展多个独立实现的证明检查内核。

这些内核可以使用不同编程语言实现，包括 Go、Rust、Haskell、C#，甚至 TeX。

通过独立实现和交叉检查，可以降低对单一实现的信任依赖。

当然，多内核检查并不意味着所有安全风险都消失了，但它提供了一种值得重视的纵深防御思路。

程序员的价值，正在从写代码转向定义正确性

回到最初的问题：当 AI 可以写代码，程序员还有什么价值？

Leo 的回答并不是程序员将会消失，而是这个职业的工作内容将发生变化。

他认为，未来软件工程师需要更加重视：

• 编写形式化规格说明。
• 定义程序应该满足的性质。
• 建立准确的系统模型。
• 理解和审查 AI 生成的证明。
• 设计复杂系统的架构与协议。
• 判断形式化模型是否真正覆盖了现实需求。

换句话说，工程师可能不再需要亲自编写每一行代码，但仍然需要知道系统应该做什么，以及如何判断它是否做对了。

Leo 甚至认为，一个人完全可能不再擅长传统意义上的编程，却依然成为非常高效、非常有价值的软件工程师。

当然，他也特别强调，底层编程能力不会消失。

汇编、操作系统、编译器、底层语言以及系统设计知识，仍然会是软件工程的重要基础。

只是整个行业的价值重心可能会向更高的抽象层迁移。

我认为，这个变化可以用下面这张图来理解：

这里还有一个值得注意的信号。

AI 不仅正在改变软件开发，也正在改变数学研究。

Mathlib 的积累、AI 自动形式化以及数学家利用 Agent 协作完成证明，都说明这种范式可能向更多领域扩散。

Leo 在访谈中还提到了金融、化学、生物学等方向。

这些领域都有大量可以数学化、模型化的知识。

当 AI 能够帮助人们把这些知识转化成机器可检查的形式化模型，形式化验证的应用边界就可能远远超出传统软件工程。

当然，不同领域的成熟程度差异很大。数学拥有相对精确的定义体系，而物理、法律和会计中往往存在现实世界的不确定性和解释空间。

因此，不能简单认为所有知识都能够被完整形式化。

但方向已经值得关注。

小结：写代码的时代正在过去？真正的变化才刚刚开始

这次 Leo de Moura 的专访，给我最大的启发并不是 Lean 有多么强大，也不是 AI 又能生成多少行形式化证明。

而是它揭示了 AI 软件工程正在发生的一次重要转变：

过去，我们主要关注如何让计算机执行我们编写的代码；未来，我们可能更加关注如何让计算机证明自己执行的代码符合我们的意图。

这两者之间有着本质区别。

AI 让代码生成成本下降，并不意味着软件开发的所有成本都会同步下降。

需求是否准确？模型是否忠实？实现是否正确？安全边界是否可靠？

这些问题不会因为 AI 写代码而自动消失。

恰恰相反，代码生成越容易，这些问题就越重要。

我尤其认同 Leo 关于规格说明的判断。

如果未来一个软件项目可以由 Agent 根据规格说明随时重新生成，那么长期真正值得维护的，可能不再只是代码仓库，而是规格说明、形式化模型、证明以及架构知识。

对于今天的软件工程师来说，我觉得至少有三个方向值得提前关注：

1. 理解形式化验证。不一定马上成为 Lean 专家，但应该理解规格说明、性质、证明和模型之间的关系。
2. 提升系统设计能力。越来越多代码交给 AI 后，定义系统边界、协议和约束的能力会更加重要。
3. 重新认识软件正确性。不要把测试通过、代码审查通过和软件正确画上等号。

最后，我想借用这次专访的核心思想，做一个判断：

AI 编程的上半场，是让机器学会写代码；下半场，则是让机器学会证明自己写的代码是对的。

而 Lean，可能正站在这场变革的一个重要起点上。

参考资料：

1. 原始专访：When AI Writes the Code, Who Proves It Works? — https://thedataexchange.media/leo-de-moura-lean-aws/
2. Lean 官方网站：https://lean-lang.org/
3. Mathlib：Lean Mathematical Library - https://github.com/leanprover-community/mathlib4
4. Aeneas：Rust Formal Verification with Lean - https://github.com/AeneasVerif/aeneas
5. Lean Kernel Arena：Lean Kernel Arena - https://arena.lean-lang.org/

还在为写 Agent 框架频频死循环、上下文爆炸而束手无策？我的新专栏 《从0 开始构建 Agent Harness》 将带你：

• 抛弃臃肿框架，回归“驾驭工程 (Harness Engineering)”的第一性原理
• 用 Go 语言手写 ReAct 循环、并发拦截与上下文压缩引擎等，复刻极简OpenClaw
• 构建坚不可摧的 Safety Middleware 与飞书人工审批防线
• 在底层实现 Token 成本审计、链路追踪与自动化跑分评估
• 从“调包侠”进化为掌控大模型边界的“AI 操作系统架构师”

扫描下方二维码，开启从 0 开始构建Agent Harness 的实战之旅。

还在为“复制粘贴喂AI”而烦恼？我的新专栏 《AI原生开发工作流实战》 将带你：

• 告别低效，重塑开发范式
• 驾驭AI Agent(Claude Code)，实现工作流自动化
• 从“AI使用者”进化为规范驱动开发的“工作流指挥家”

扫描下方二维码，开启你的AI原生开发之旅。

商务合作方式：撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。如有需求，请扫描下方公众号二维码，与我私信联系。