从零开始用 Lean 4 证明操作系统关键性质：第一个定理实战指南

操作系统形式化验证，听起来像是一个离普通开发者很远的话题，但它解决的是写系统代码时最扎心的一个问题：你怎么知道你的代码“真的”是对的？这篇教程用 Lean 4 带你走通“证明第一个定理”的完整流程，从环境搭建、项目初始化到归纳法证明，不绕弯子，直接上手。这篇内容不适合想三天掌握验证全貌的人，适合愿意花一个晚上亲手把第一个证明敲出来的人，敲完你会对整个形式化验证的思路有一个完全不同的感觉。

1. 先搞明白：操作系统为什么要“证明”定理

1.1 从“测试通过”到“证明正确”

我最早听到“形式化验证”这个词，是在一个做过嵌入式安全系统开发的朋友嘴里。他们团队维护的调度器代码，每个版本都要过几百条测试用例，覆盖率报告漂漂亮亮，但一上高负载、多核并发场景，还是能翻出毛病。原因很简单：测试只能覆盖你写得出来的那些场景，而操作系统面对的输入组合几乎是无穷无尽的。中断可以发生在任意指令边界，线程切换可以打断任意临界区，资源请求顺序可以任意交错。你永远没法保证“这版代码覆盖了所有情况”。

形式化验证换了一种思路：不靠跑例子，而是把程序行为转换成数学命题，再用逻辑规则严格推导出“这个性质对所有可能的执行路径都成立”。测试是在一堆样本上确认程序没出错，证明是在整个状态空间上断言程序不可能出错。这两件事有一个本质区别：测试能证明一个 bug 存在，但永远不能证明 bug 不存在；证明虽然费劲，但一旦证完，性质就是板上钉钉的。

对操作系统来说，这种“板上钉钉”值钱在哪？消息队列的追加顺序、内存分配的不变量、调度器状态机的迁移合法性，这些模块一旦出错，问题往往不是简单的功能异常，而是系统崩溃、数据损坏、安全漏洞。用定理证明给这些关键性质上“保险”，在工业界已经有不少实际投入，特别是在微内核、可信固件、实时控制系统这些领域。它不是要替代测试，而是在测试之上加一道数学级别的兜底。

1.2 定理证明在系统验证中的典型位置

形式化验证其实是个大箩筐，里面装着模型检测、抽象解释、符号执行、定理证明等一堆工具。它们各有各的主场。模型检测适合验证有限状态系统的时序性质，比如死锁不会发生；抽象解释适合做静态分析，比如数组越界、空指针；而定理证明适合处理那些状态空间无限、需要归纳推理的问题，比如“无论队列里塞多少条消息，先进先出的顺序都不会乱”。

定理证明的特点是可以处理无限状态空间，代价是费人。你需要把一个复杂的系统性质拆解成大量可被机器检查的中间步骤，这个过程很像写数学证明：先建立定义，再施加归纳假设，最后逐步化简。证明工具本身则负责守住纪律，每一步推导都必须符合逻辑规则，不允许“显然成立”这种带主观性的跳跃。

Leans 的交互式证明体验在这方面做得特别顺手。你写下一行 tactic，它马上反馈当前要证的目标长什么样、手头有哪些可用的假设，有点像边写代码边看调试器输出。对写过代码的人来说，这种反馈循环非常容易适应。

1.3 为什么选 Lean 作为第一语言

可以选的形式化验证工具其实不少，Coq、Isabelle、Lean 各有各的拥趸。我最后在这次教程里选 Lean 4，主要是三个原因。

第一，安装和上手成本低。一套工具链命令装完，VS Code 装个插件就能用，和写普通代码的体验很接近。第二，Lean 对自动化的支持比早期版本强了不少，简单目标可以一两行 tactic 收掉，不用在琐碎的细节上耗尽耐心。第三，它跟函数式编程的思路一致，做定义、做模式匹配、做递归都非常自然，对习惯写 Haskell、OCaml、Rust 这类语言的开发者来说，切入成本很低。

当然，这不代表其他工具不好。只是作为“证明第一个定理”这个目标，Lean 能让你的注意力集中在理解归纳法、理解定义展开这些核心概念上，而不是先和工具链搏斗三小时。

2. 搭建证明环境：Lean 4 安装与项目初始化

2.1 安装 Lean 4 工具链

Lean 4 在 2021 年正式发布之后，安装方式已经收敛到一套脚本流程。它在不同平台上的安装方式几乎一致，在 Linux 和 macOS 上尤其省事。

在终端执行这一行，会安装 Lean 的版本管理器和构建工具：

curl -fsSL https://get.lean-lang.org/lean4 | bash source ~/.elan/env lean --version

如果是在 Windows 上，我不太建议直接在原生终端折腾，更常见的选择是装了 WSL 后在 Linux 环境里跑，因为后续很多系统编程相关的验证项目默认也是以类 Unix 环境为前提的。

安装完以后，你可以把elan理解为 Lean 世界的版本管理器，类似 Node 生态里的 nvm。它的作用是把多个 Lean 工具链隔离开，不同项目可以锁定不同版本，不会因为某个项目更新了依赖导致其他项目全部崩掉。这个设计对于后面要接触真实系统验证项目的人来说很重要，因为验证项目往往对工具链版本非常敏感，一个版本升级可能意味着某个库不再兼容。

2.2 用 lake 初始化一个验证项目

Lean 4 的项目管理和构建工具叫 lake，你可以把它类比成系统开发里常见的构建脚本工具。创建项目：

lake new formal_os cd formal_os

这个命令会生成一个最小的 Lean 项目骨架，里面有lakefile.toml、Main.lean等基础文件。lakefile.toml是项目的配置入口，类似系统的配置清单，依赖项、构建选项都会写在这里。Main.lean则是默认的入口模块，我们后续的验证代码可以直接写进去，或者新建一个Test.lean再被Main导入。

首次在编辑器里打开这个项目时，Lean 会自动解析依赖并构建底层库，这一步可能需要一点时间，因为 Lean 标准库的导入和编译比想象中要重。看到 VS Code 右下角出现进度提示，别急着操作，等它跑完。

2.3 编辑器配置与第一个“证明”运行

VS Code 里搜索并安装名为 “Lean 4” 的官方插件。装好后打开项目目录，左侧会出现一个独立的 “Lean Infoview” 面板。这个面板是整个证明过程的主战场：你写的每一行 proof 脚本执行完，它都会实时更新当前证明目标。

用 VS Code 打开项目后，把Main.lean的内容替换成下面这段最简单的代码：

example : (1 : Nat) + 1 = 2 := by rfl

光标停留在rfl那一行时，Infoview 会显示这条证明的状态。如果所有目标都被关闭，它会在末尾提示这个example证明成功。

这就是你的第一个形式化证明。虽然它小得不能再小，但里面的核心流程和一套几百行的验证工程完全一致：写出一个命题，用证明脚本构造推理链，最后让工具确认每一个步骤都合法。

3. 第一个定理：从 1+1=2 到归纳法

3.1 用 rfl 证明 1+1=2

先盯着上面那个rfl看一会儿。为什么这个证明只有一行，而且不需要任何额外知识？关键在于rfl处理的是“定义性相等”：两边在展开定义之后，是不是逐字逐句相同。

在自然数类型里，1其实就是Nat.succ 0，2就是Nat.succ (Nat.succ 0)。加法Nat.add的定义方式是这样的：

0 + b = b Nat.succ a + b = Nat.succ (a + b)

所以1 + 1会按定义一步步展开：先变成Nat.succ 0 + Nat.succ 0，然后根据第二条规则变成Nat.succ (0 + Nat.succ 0)，再根据第一条规则变成Nat.succ (Nat.succ 0)。这个东西恰好就是2。

rfl这个 tactic 做的事情就是检查等式两端能不能通过这种定义展开完全重合。能重合，证明就结束；不能重合，它就会报错。这个概念在系统验证里非常有用。很多系统正确性中看似“自己当然是对的”的部分，本质上都是定义性或者平凡推导就能解释的，形式化工具不允许你跳过，但也会用这种方式告诉你：这里确实是稳的。

3.2 加法结合律：第一个真正需要脑子的定理

1+1=2 太简单了，承载不了形式化验证的核心思想。我们把目标升级成一个在数学上“显然”但在证明上需要技巧的定理：加法结合律。

如果你直接用 Lean 标准库里自带的加法，simp大概率会在后台偷偷调用标准库已有的结论，导致读者产生“怎么什么都没干就证完了”的错觉。为了看清每一步推理，我在这里自定义了一个完全独立的加法函数myAdd，它没有任何预设定理，所有性质都得我们自己证。

namespace MyNat def myAdd (a b : Nat) : Nat := match a with | Nat.zero => b | Nat.succ a' => Nat.succ (myAdd a' b) theorem myAdd_assoc (a b c : Nat) : myAdd (myAdd a b) c = myAdd a (myAdd b c) := by induction a with | Nat.zero => rfl | Nat.succ a ih => simp [myAdd, ih] end MyNat

把这段代码贴进Main.lean再跑一下，你会看到两个分支都成功关闭。但成功归成功，你得理解simp [myAdd, ih]到底干了什么。

先看Nat.zero分支。此时a被替换成Nat.zero，目标变成：

myAdd (myAdd 0 b) c = myAdd 0 (myAdd b c)

myAdd 0 b按定义直接化简成b，myAdd 0 (myAdd b c)也按定义直接化简成myAdd b c。左右两边都变成myAdd b c，rfl收工。这一分支相当于证明了“第 0 级台阶能站住”。

再看Nat.succ a分支。此时归纳假设ih已经替我们声明了：

myAdd (myAdd a b) c = myAdd a (myAdd b c)

目标是：

myAdd (myAdd (Nat.succ a) b) c = myAdd (Nat.succ a) (myAdd b c)

simp [myAdd, ih]会把myAdd按定义展开，并用ih做改写。完整的推导链是这样的：

myAdd (myAdd (Nat.succ a) b) c = myAdd (Nat.succ (myAdd a b)) c = Nat.succ (myAdd (myAdd a b) c) = Nat.succ (myAdd a (myAdd b c)) -- 在这里使用 ih = myAdd (Nat.succ a) (myAdd b c)

说到底，归纳证明就是递归定义的镜像。myAdd依赖第一个参数递归，证明也围绕第一个参数递归展开。第 0 级站住了，如果站在第 a 级能推算到第 a+1 级，那么整个阶梯就全部贯通。这就是数学归纳法，也是形式化验证处理无限状态空间的基本武器。

3.3 读懂 Lean 在背后的反馈

如果你在 VS Code 里亲手敲这段代码，会看到induction a with之后 Infoview 里出现两个新的证明目标，每个目标的上下文都包含当前分支可用的假设。尤其注意Nat.succ a ih这一行，ih就是归纳假设，它是自带的，不需要你手动声明。很多人第一次写归纳证明时会觉得“这是不是作弊了，我什么都没做结论自己就出来了”。不是作弊，这是逻辑规则：归纳法允许你使用一个针对更小规模的结论。

从这个角度再看定理证明的过程，它和写普通代码有一个很微妙的相似之处：你不需要记住每一步的细节，需要的是在正确的层次上把正确的“引理”组合进去。只不过普通代码组合的是函数调用，证明组合的是逻辑推理规则。

4. 一个更接近操作系统的定理：消息队列追加结合性

4.1 从代数到系统：为什么抽象定理有用

自然数加法的结合律看起来和操作系统毫无关系。但如果你换一个视角，把自然数看成抽象的“资源计数”，把加法看成“资源合并”，结合律说的就是“合并的顺序不影响最终总量”。在操作系统的内存分配、任务队列合并、日志批处理场景里，这种性质比表面看上去要重要得多。

为了不让讨论停留在“以后可能有用”的层面，我直接造一个更贴近系统的例子：消息队列的追加操作。假设我们维护一个消息队列，每条消息有编号和内容，整个队列建模成List Msg。向队列追加一批消息，等价于把两条列表拼在一起。

structure Msg where id : Nat payload : String def enqueueAll (xs ys : List Msg) : List Msg := match xs with | [] => ys | x :: rest => x :: enqueueAll rest ys

这里的enqueueAll外表看就是一个列表拼接，但从语义上它表示的是“把消息队列xs整体追加到队列ys后面”。对这样的系统操作，我们要问一个非常实际的问题：如果一批消息要经过两次合并，最终到达目的队列，不同的合并顺序会不会影响消息顺序？

4.2 用归纳法证明追加结合律

直观上消息顺序不会变。要证明它，就是要证下面这条定理：

theorem enqueueAll_assoc (xs ys zs : List Msg) : enqueueAll (enqueueAll xs ys) zs = enqueueAll xs (enqueueAll ys zs) := by induction xs with | List.nil => rfl | List.cons x rest ih => simp [enqueueAll, ih]

这里的证明结构和上一次的加法结合律几乎一模一样。List是个递归类型，所以归纳这两个字在这里同样适用。

List.nil分支对应空队列。空队列追加什么都不改变，所以左右两边化简完是同一个表达式，rfl直接收掉。

List.cons x rest分支对应“队列里至少有一条消息 x，其余消息是 rest”。此时归纳假设ih声明了：

enqueueAll (enqueueAll rest ys) zs = enqueueAll rest (enqueueAll ys zs)

然后simp展开enqueueAll的定义，把公共的头元素x提到最外层，再使用ih处理剩下的部分。推理链大概是：

enqueueAll (enqueueAll (x :: rest) ys) zs = x :: enqueueAll (enqueueAll rest ys) zs = x :: enqueueAll rest (enqueueAll ys zs) -- 使用 ih = enqueueAll (x :: rest) (enqueueAll ys zs)

这个证明跑通后，我们获得了关于消息队列的一条不变量：合并顺序不影响最终消息排列。这不是靠跑了几千组随机测试得到的统计信心，而是对所有可能的队列内容都成立的性质。

4.3 系统里大量正确性依赖这类“显然”

在真实的系统验证里，像“队列合并顺序无关”这种结论往往只是整个验证工程的一小块拼图。它不会直接让你证明调度器没有竞态，但它会成为你的证明工具箱里的一个基础引理，被后续更复杂的定理反复调用。

我之前说过，测试和证明的根本差异就在这种地方。测试跑一万遍，你只能对“这一万遍”有信心；证明写完一遍，你得到的结论覆盖了“所有情况”。系统代码之所以适合形式化验证，正是因为它的正确性往往是组合式的：关键模块由小到大、逐层组合，每层的组合性质如果都能用定理锁定，整个系统的正确性就有了牢固的地基。

5. 实操中的高频翻车与排查技巧

5.1 类型对不上时先看哪里

Lean 的类型错误信息通常比较直接，但对新手来说还是容易看懵。最常见的一类问题是类型不匹配：比如函数的某个参数期望的是Nat，你传了一个String；或者模式匹配的分支写错类型，导致左右两边类型对不上。

遇到这种问题，第一件事不是盯着那一大段红色波浪线看，而是把 Infoview 打开，看当前目标⊢后面是什么，上下文里有哪些变量和假设。绝大多数报错，最后都能归结为“当前目标的形状和证明脚本的操作不一致”。养成看上下文的习惯，比强行背错误信息有效得多。

5.2 归纳变量选错：一个经典卡点

加法结合律是个特别好的反面教材。如果当时我选择对b做归纳而不是对a做归纳，这个证明会卡到你怀疑人生。

原因在于myAdd是按照第一个参数递归定义的。对b归纳时，Nat.zero分支的目标里有myAdd a 0这样的表达式，因为a是个任意变量，myAdd a 0无法按定义继续展开。你手里没有针对a的任何归纳假设，所以只能卡在原地。

这个经验在验证真实系统代码时经常遇到：定理能不能证下去，很多时候取决于你把归纳放在哪一个变量上。判断依据就是看哪一个参数驱动了递归定义的模式匹配。驱动递归的那个参数，通常才是归纳的首选对象。

5.3 小心“证明太容易”的陷阱

还有一种反直觉的坑，出现在你飞快写完一个simp然后发现证明通过的情况。在标准库里，列表的追加结合律是已经存在的定理。如果你直接拿标准库函数写代码，simp可能会悄悄调用这些现成定理，让你以为形式化验证就是“敲一行，自动搞定”。这种错觉会在你遇到真实项目时迅速破灭，因为真实场景的大部分目标都没有现成定理可用，必须靠你手动选择归纳变量、设计中间引理、拆分情况。

所以我在这篇教程里故意绕开标准库的现成结论，用自定义的myAdd和enqueueAll把推理过程暴露出来。形式化验证的难点从来不是最后合并那些小步骤，而是搞清楚“哪些步骤是平滑的、哪些步骤需要先建立引理”，这一层判断力只有靠亲手推导才能培养。

最后留一句个人的感受

我第一次在 Lean 里证明加法结合律时，那个定理用大白话说三秒就能讲完，我却花了将近一小时才彻底搞懂归纳假设是怎么递推下去的。后来转去做消息队列类似性质时，才意识到对“显然”保持耐心，恰恰是操作系统验证最需要的素质。这里的每一项证明都在教你同一件事：不要凭感觉相信代码，把一切写成能接受检查的步骤。建议你把这篇文章里的三段代码亲手敲一遍，第一次跑通第一个定理之后，再回头去看那些动辄成千上万行验证工程，视线会清晰很多。