Lean 与 AI 辅助软件开发：从代码生成到形式化验证 • Misaka Cloud Blog

AI 擅长快速生成实现；Lean 的价值，是把关键规则写成可由小型可信核心检查的命题。

1. 从“生成得快”到“为什么可信”

AI 辅助编程显著提高了代码生成速度，但速度并不等于可靠性：

生成的代码可能包含隐藏缺陷；
测试只能覆盖选定的输入与执行路径；
当代码量迅速增长时，完整人工审查越来越困难；
自然语言需求本身可能含糊、遗漏条件，甚至互相矛盾。

Lean 在这条链路中适合承担的不是“再写更多代码”，而是规格与证明的检查层：

用户需求
    ↓
形式化规格
    ↓
AI / 人类生成实现与证明
    ↓
Lean Kernel 检查证明
    ↓
接受，或返回错误继续修改

这里最重要的变化，是把“看起来正确”变成“在明确写出的假设与规格下，存在一份可机械检查的证明”。

2. Lean 是什么

Lean 4 既是一门函数式编程语言，也是一套交互式定理证明器。它允许开发者把下列对象写成精确、可检查的形式：

数学定义与定理；
数据结构的不变量；
算法输入、输出之间的关系；
协议允许的状态转换；
业务系统必须保持的守恒条件。

例如，“排序算法正确”不能只写成一句模糊的“输出排好序了”。更完整的规格至少包含两部分：

1. 输出序列有序；
2. 输出与输入包含相同的元素及其重数。

第一条排除了乱序，第二条排除了丢失、复制或凭空增加元素。Lean 可以分别定义这些性质，再要求实现或抽象模型提供证明。

形式化验证的难点也正在这里：Lean 只会严格检查已经形式化的命题。规格若漏掉第二条，即使“有序性”的证明完全正确，一个总是返回空列表的实现仍可能满足这份残缺规格。

3. 为什么可以让 AI 参与证明

Lean 的关键设计之一，是使用相对小型的可信核心（kernel）检查证明项：

人类 / AI
    ↓
策略、自动化、证明搜索
    ↓
生成证明项
    ↓
Lean Kernel
    ↓
接受 / 拒绝

AI、自动化策略和证明搜索器都可能犯错。它们的输出不能因为“像证明”就被接受，而必须通过 Kernel 的类型检查。错误的步骤无法组成目标命题所要求的证明项，因而会被拒绝。

这使 AI 很适合充当证明搜索助手：它可以尝试引理、补全证明、解释错误并反复修正；最终是否成立，不由 AI 自己宣布，而由 Lean 检查。

不过，“Kernel 接受”并不等于整个现实系统绝对无误。可信边界仍包括形式化规格、Lean 的可信计算基础，以及从模型连接到实际程序的过程。形式化方法缩小了需要信任的范围，但不会让建模错误自动消失。

4. Lean 与 Rust：解决不同层次的问题

Rust 与 Lean 都试图在运行之前排除错误，但它们关注的层次不同。

Rust 通过所有权、借用检查、类型系统等机制，静态排除大类内存安全与并发错误。例如：

let x = String::from("hello");
drop(x);
println!("{}", x);

x 已被移动给 drop，后续访问会被编译器拒绝。开发者不需要为每次移动手写数学证明；规则已经内建在语言与编译器中。

Lean 则允许开发者定义更贴近问题领域的性质，例如：

排序结果既有序又不丢元素；
转账前后的系统总金额守恒；
状态机不会进入非法状态；
密码算法的实现满足某个数学定义；
编译器变换保持程序语义。

可以把二者的侧重点概括为：

工具	主要职责
Rust	工程实现、性能、所有权与内存安全
Lean	数学性质、逻辑规格及其证明
测试	在选定场景中观察真实运行行为
AI	生成候选代码、规格、测试与证明尝试

它们不是互相替代的关系。Rust 的安全保证并不自动推出业务逻辑正确；Lean 中证明的抽象模型，也不会自动等同于生产环境里的 Rust 二进制。

5. 一个带非零证明的除法接口

普通 Rust 函数可以接收零作为除数，是否处理这一情况取决于接口与实现：

fn divide(a: i32, b: i32) -> i32 {
    a / b
}

在 Lean 中，可以把“除数不为零”直接放进函数类型：

def safeDiv (a b : Int) (_h : b ≠ 0) : Int :=
  a / b

#eval safeDiv 10 2 (by decide)

参数 _h : b ≠ 0 是一个显式证明参数。调用者不仅要提供 a 与 b，还要提供 b ≠ 0 的证明。对常量 2，by decide 可以完成这个可判定命题；对 0，则无法构造 0 ≠ 0 的证明。

这个例子展示的是如何让非法输入难以表达。它没有证明整数除法的更多性质，也没有自动说明某段 Rust 代码与该定义一致。需要什么保证，仍必须继续写进规格并完成相应证明。

6. Lean 在 AI Coding 中的实际位置

验证关键算法

AI 可以生成排序、搜索或优化算法；形式化规格则定义输出必须满足的条件。随后由人类、AI 或自动化工具尝试完成证明，Lean 负责最终检查。

候选排序实现
    +
输出有序
    +
元素及重数保持不变
    =
需要检查的完整正确性目标

验证业务不变量

以转账为例，可以先在模型中定义账户余额与状态转换，再声明：

转账前系统总金额 = 转账后系统总金额

如果候选模型错误地给收款方增加两倍金额，守恒性证明将无法完成。这里 Lean 检查的是形式化模型；要把结论扩展到真实服务，还必须证明或验证真实实现遵循同一状态转换。

安全关键组件

形式化方法尤其适用于错误代价高、核心逻辑相对稳定的部分，例如：

密码协议与算法；
编译器关键变换；
操作系统内核机制；
网络协议状态机；
金融系统的核心不变量。

实践中通常不会一开始就验证整个产品。更现实的路径，是先识别最关键的不变量与最小可信组件，把证明成本集中在最值得保证的地方。

7. Rust 与 Lean 怎样连接

一个常见的项目布局可能是：

project/
├── src/
│   └── transfer.rs       # Rust 工程实现
├── tests/
│   └── transfer.rs       # 可执行测试
└── specs/
    └── transfer.lean     # 抽象模型、规格与证明

但把两个文件放在同一仓库，并不会自动证明它们一致。至少还需要一座“桥”：

人工对应：审查 Rust 实现是否忠实实现 Lean 模型，成本较低但仍依赖人工；
受控代码生成：从经过证明的模型生成部分实现，减少两份逻辑漂移；
语义翻译或验证工具链：把源代码或中间表示映射到可证明的模型，再证明精化关系；
运行时检查与测试补充：覆盖外部系统、I/O、部署配置等未被模型包含的部分。

因此，现阶段更准确的表达不是“Rust 代码会自动变成 Lean 证明”，而是：

Rust 实现
    +
Lean 模型与规格
    +
连接实现和模型的可信过程
    +
证明、测试与审查

AI 可以帮助生成这几部分，但不能省略它们之间的对应关系。

8. 最重要的能力边界

Lean 的价值不是承诺“程序一定没有 bug”，而是：

对已经明确形式化的规则，要求给出可由可信核心检查的证明。

它能显著提高保证强度，同时也把问题推向更根本的一层：我们究竟想保证什么？假设是否完整？模型是否覆盖了真实实现与运行环境？

未来高可靠 AI 软件开发可能形成这样的分工：

AI：快速生成候选实现、测试与证明
Rust：提供工程实现能力和底层安全约束
Lean：检查关键逻辑的形式化规格与证明
测试：覆盖真实集成路径与模型之外的环境
人工审查：确认需求、规格和系统边界

当 AI 让“生成”越来越便宜时，规格、验证与可信连接会变得更重要。Lean 的意义不在于限制生成速度，而在于为关键结论提供一条可复核的证据链。

整理自 2026-07-19 技术讨论，经人工审校。