上一讲讨论了规格与实现之间的距离，也就是 spec-impl gap。程序里存在缺陷（fault），不代表这次运行一定进入错误状态（error）；进入错误状态，也不代表用户马上就能看到异常（failure）。测试设法触发隐藏的缺陷，断言帮助我们尽早观察到错误。但要把这些事情做好，最终仍然需要架构，以及设计实验的聪明才智。
例如，让 Agent 为项目添加多个层级的测试，它很容易给出一份“合理”的目录：在 tests/ 下建立 unit/、module/ 和 system/，再用一个 justfile 提供执行入口。这当然可以作为起点。但新增一种需要虚拟机的测试时，目录、文档、CI 配置和执行脚本要改几处？如果四处各写一遍测试策略，迟早会出现文档说要跑、CI 却没跑的情况。
我们可以稍稍换一种做法：在 docs/testing.md 中维护一张表，让它成为测试策略的唯一事实来源（Single Source of Truth）。
| Scope | Level | Runner | Args | Metadata |
|---|---|---|---|---|
| crates/* | unit | cargo-test | --workspace | fast |
| packages/* | unit | bun-test | fast | |
| tests/modules/* | module | script | isolated | |
| tests/system/* | system | qemu-test | requires-vm |
Scope 表示规则覆盖哪些目录，Level 表示测试层级，Runner 和 Args 描述如何执行，Metadata 则记录“运行很快”“需要隔离”“依赖虚拟机”等属性。人可以阅读这份文档，Agent 可以维护它，执行器可以直接解析它生成执行计划，CI 可以检查它与仓库是否一致。机器可读和人类可读，并不一定要分成两份文件。
这里的关键是 Registry ↔ Repository 的双向核对。表声明“应该怎样跑”，仓库提供“实际有什么”。不仅要检查表里的路径是否还存在，还要独立扫描仓库，检查新加入的测试是否被登记。假如执行器只遍历表中出现的路径，那整片没登记的测试就会悄悄消失，CI 仍然一片绿色。
Agent 的局限在这里很具体：它擅长补全一种常见组织形式，却未必主动重新设计信息的归属和反馈方式。弥补这个缺口，不能只说“请更聪明一些”，而要把约束变成它能看到、能检查的对象。例如要求新增测试必须登记，运行仓库与注册表的一致性检查，让遗漏产生明确失败。人的架构判断由此变成 Agent 可以持续维护的机制。
测试可以揭示 bug 的存在，通常却不能证明 bug 不存在。跑过一万个输入，仍然可能漏掉第一万零一个。那么，能不能像证明数学定理一样，证明程序符合规格？
这个愿望几乎与计算机本身一样古老。1949 年，Turing 已经讨论过如何检查一个程序；McCarthy 在 1960 年代提出，不仅应该证明程序满足规格，证明本身也应该交给计算机检查。Floyd 在 1967 年的工作中把断言放到控制流上，Hoare 在 1969 年进一步给出程序推理的公理化框架。它们共同指向一个大胆的想法：程序执行有明确规则，因而程序性质也可以成为演绎推理的对象。参见 Turing 的原始档案、McCarthy 的论述和 Hoare 的论文。
Hoare 三元组把问题写成：
其中， 是前置条件， 是程序， 是后置条件。它表达的是：从满足 的状态开始执行 ，如果执行终止，那么结束状态满足 。例如，在数学整数上，从 出发执行 x := x + 1，就可以推出 。如果讨论的是真实机器整数，还必须把溢出等规则纳入语义。
“如果终止”不能偷偷省略。部分正确性说明程序结束时结果正确；总正确性还需要证明它确实会结束。一个永远不返回的排序程序，不能因为从未返回错误结果，就算实现了我们想要的排序功能。
数组不会越界、指针不会指向非法位置、数据结构始终满足约束，都可以写成数学性质。难点在于找到合适的规格和证明，而不是在代码旁边加一句“已验证”。这也不意味着存在一个万能算法，可以自动判断任意程序的任意性质。
循环可能执行任意多次，我们如何用有限篇幅证明它？常见办法是寻找不变式（invariant）：一个在循环开始前成立、每次执行循环体后仍然成立的命题。
设循环条件为 ，循环体为 ，不变式为 。证明分成三步：初始条件能推出 ；在 与 成立时执行 ，仍然得到 ；退出循环时， 与 一起推出目标。我们没有逐次枚举所有循环，而是找到了一条能贯穿任意多轮执行的规律。
看一个班级投票的例子：如果有一个选项得到严格超过一半的票，怎样只用一个候选人和一个计数器找到它？Boyer–Moore 多数投票算法的核心非常短：
candidate, cnt = None, 0
for vote in votes:
if cnt == 0:
candidate = vote
if vote == candidate:
cnt += 1
else:
cnt -= 1
看起来有些神奇：遇到相同选项就加一，不同就减一，计数归零后换候选人。为什么最后留下的一定是多数？cnt 显然不是候选人的真实得票数。
真正的不变式是：已经读过的所有票，都可以分成若干对选项不同的票，以及 cnt 张全部投给 candidate 的剩余票。 初始没有票，这个命题成立。新票与候选人相同，就加入剩余票；新票不同，就与一张剩余票配成一对；没有剩余票时，新票自己成为新的候选人。每一步都保持这个分解。
再看多数的性质。如果某个选项的票数严格超过其他选项票数之和，删掉一对不同的票，无法消除它的优势：这对票至多包含一张多数票。如果包含一张，多数票和其他票各少一张；如果不包含，多数的优势反而扩大。于是，把那些不同选项的票对全部抵消后，严格多数仍然必须留下。根据不变式，剩余票全属于 candidate，所以它就是要找的答案。
这里的前提“存在严格多数”很重要。如果没有这个保证，第一遍只能产生候选人，还要第二遍统计它是否真的超过一半。例如 A, B, C 最后留下 C，但它并不是多数。证明不仅告诉我们代码为什么正确，还准确指出了它在什么条件下正确。算法及其机械证明的背景可参见 Boyer 与 Moore 的原文。
这个例子的巧妙之处，是把不断变化的计数器解释成“抵消后的余量”。代码只有几行，找到这个解释却需要理解。把同样的工作扩展到复杂指针、内存分配器和整个操作系统，证明成本就很快超过了普通项目能承受的范围。
如果手工寻找逻辑证明太难，还可以换个角度：程序就是状态机。状态包含变量、内存、各线程执行到哪里；执行一步，就是从一个状态转移到另一个状态。编程语言的操作语义（operational semantics）正是在描述这样的转移规则。
对一个有限状态模型，可以从初始状态出发，不断加入所有可能的后继，直到不再出现新状态。如果所有可达状态都满足安全性质，就完成了这个模型上的证明。这就是模型检查（model checking）最直观的出发点：用穷举证明。
上一讲的并发计数器，可以拿来做一个很小的模型。假设 sum 是初值为 0 的原子整数，两个线程各运行一次下面的循环，即 N = 1，原子读写采用顺序一致语义：
void T_sum() {
for (int i = 0; i < N; i++) {
int t = atomic_load(&sum);
t++;
atomic_store(&sum, t);
}
}
我们的要求是：两个线程结束后，sum == 2。但存在这样的执行：线程 A 读到 0，线程 B 也读到 0；A 在自己的局部变量中算出 1，B 也算出 1；两者先后把 1 写回。最终结果是 1。
模型检查器可以系统地探索这些交错，并给出通向错误状态的轨迹。修复方案可以是把加一变成一个原子的读改写操作，也可以用锁保护整个过程；随后应针对修复后的转移规则重新检查性质。这里的小模型并没有顺带证明任意线程数、任意循环次数下的全部性质，它准确回答的是我们交给它的模型问题。
为什么完整穷举能算证明，而多跑几次测试通常不算？区别在于是否已经覆盖全部允许行为。设探索得到的状态集合为 ：它包含初态，而且对转移封闭，也就是其中任意状态的任意后继仍在 中。于是“所有可达状态都在 中”本身就是一个归纳不变式。只要 中没有坏状态，坏状态就不可达。
麻烦是状态爆炸：多个组件各有一些状态，组合起来的状态数可能成指数增长。因此，模型检查的发展很大程度上是在改变“如何表示和搜索这些状态”。符号模型检查用布尔公式、二叉决策图等结构表示一整组状态，不必逐个存储；有界模型检查把“是否存在至多若干步就出错的执行”编码成 SAT，即布尔可满足性问题。后者找到解就得到反例，但在某个步数界限内无解，还不能自动推广到任意长度。经典论文 Symbolic Model Checking: 10²⁰ States and Beyond 的标题，就体现了改变表示方法的力量。
另一个方向是让搜索帮助发现证明。粗略模型可能包含真实系统中不可能出现的反例，这时可以补回必要细节，再继续检查；也可以逐步生成归纳引理，排除一批不可能到达的坏状态。IC3 的论文展示了后一种思路。前面要求程序员费劲想出的 invariant，也可以成为算法搜索的产物。
人类从未放弃过把证明带进真实软件，只是选择了不同的切入点。
TLA+ 从模型出发。以事务提交为例，我们关心的核心问题可以是：参与者是否可能出现一个已经提交、另一个已经中止的矛盾结果？建模时先描述参与者状态、消息和允许的转移，再检查一致性性质。模型暂时不需要包含网络库怎样分配缓冲区、日志怎样格式化等实现细节，因而有机会把精力集中在协议本身。
但简化模型正确，为什么能说明真实系统正确？中间需要一座桥，叫 refinement（精化）：说明具体系统的行为如何对应到抽象模型的行为。一个具体步骤可能对应模型中的一步，也可能只是抽象状态不变的“停顿”；整体上必须保持要证明的关系。比如具体时钟每分钟变化一次，只观察小时数时，大多数步骤就表现为停顿。这类关系才让抽象层的性质能够约束具体层。参见 Lamport 的 Refinement in State-Based Formalisms；更深入的理论背景是 Abadi 与 Lamport 的 The Existence of Refinement Mappings。证明模型并不会自动补上实现与模型之间的这座桥。
KLEE 从程序路径出发。普通执行给输入一个具体值，符号执行则把输入保留为符号；遇到分支时，把分支条件加入路径约束。例如一个函数按 x == 0、x < 0、其余情况分别返回 0、-1、1，所有输入就按执行路径分成零、负数和正数三类。不必分别运行每一个整数，一条符号路径就可以代表一整类输入。KLEE 的入门教程用的正是这样的例子。
假设当前路径约束为 ，我们希望该路径满足性质 ，就可以询问求解器： 是否有解？有解，说明存在一个沿这条路径执行却违反性质的输入；无解，说明在所采用的语义和约束下，这条路径上的输入不会违反 。把输入按路径分组，并不意味着所有相似路径都能自动合并；循环、路径数量和外部环境仍然会限制搜索。
还有人直接选择了证明真实基础软件。CompCert 证明编译过程保持程序语义，让源码上的性质能够传递到编译后的程序。2009 年论文报告的形式化与证明约为 3 人年、4.2 万行 Coq，其中 76% 是证明。seL4 则证明内核 C 实现符合抽象规范；首次完成时，整个设计、文档、实现与验证约投入 25 人年，证明脚本约 20 万行。这些数字描述的是当时的项目范围，不是今天所有版本的统一统计。参见 CompCert 论文和 seL4 项目统计。
为什么值得为编译器和内核付出这样的代价？因为它们是许多软件共同依赖的基础。一个编译错误可能破坏上层费尽力气证明的性质，一个内核错误可能影响整个系统。证明成本虽然昂贵，却有机会在每次编译、每次系统调用中反复受益。疯狂的事情还是有人做，而且会被历史记住。
要理解 AI 为什么可能改变证明的成本，先看 proof assistant，也就是证明助手。
课堂上写数学证明，经常省略“显然”的中间步骤。改卷人可能理解了我们的意思，也可能被一段看起来很像证明的话糊弄过去。证明助手把工作台变得十分严格：一边列出“已知什么”，另一边列出“还要证明什么”，我们只能通过允许的规则改变证明状态。
比如用一个已知等式改写目标，或者应用一个定理，把“证明结论”变成“分别证明这个定理需要的前提”。当目标恰好已经是一个已知事实，就可以引用它，关闭这个目标。不是敲一句“显然成立”，计算机就会通融。
下面用概念伪命令说明几种基本操作；它们不是要求照抄运行的 Lean 语法。
choose A，选出一个具体同学，再证明 。只报名字不够，还得拿出他满分的证据。intro x，任取一名同学，再证明 。这里的“任取”意味着不能偷偷假定他是班里的学霸。intro h，把 加入已知，再在这个假设下证明 。induction n 拆成基础情形 ，以及从 推出 的归纳步骤。于是，证明变成了一连串有明确输入、明确输出、明确合法性条件的操作。复杂的证明策略可以替我们搜索步骤，AI 也可以尝试生成这些操作，但最终构造出的证明对象仍需要被内核检查。Lean 的 tactic 文档将 tactic 描述为构造证明的专用程序语言。
这种反馈对 Agent 极其有用。它不再只能反复问另一个模型“你觉得我的证明对吗”，而是可以运行检查，看到哪个目标没有完成、哪个类型不匹配，再修改。创造证明很难，检查一个已经写清楚的证明却可能机械得多。
Curry–Howard 对应进一步把这个工作台与编程联系起来：命题对应类型，证明对应这个类型的对象。证明 ，就像构造一个函数 ：给它一个 的证明，它就产生一个 的证明。
最简单的例子是 。对应程序就是恒等函数：
(x: P) => x
输入已经是 类型的对象，直接返回它，就完成了要求。这里没有任何魔法，但逻辑中的“由 P 可得 P”确实变成了程序中的类型匹配。
存在性证明则可以理解为把见证和证据装在一起。选定同学 A，再提供 p: P(A)，就得到 [A, p]：不仅告诉我们谁满足条件，还提供他满足条件的证明。蕴含证明是在假设 h: H 下构造 Q，最后把构造过程封装成一个从 H 到 Q 的函数。
归纳证明也能写成递归程序。假设 base 是 的证明，step 能把 的证明变成 的证明，那么下面的依赖类型伪代码就描述了对任意自然数构造证明的方法：
base: P(0)
step: (k: Nat, ih: P(k)) => P(k + 1)
f(n: Nat): P(n) =
if n == 0 then base
else step(n - 1, f(n - 1))
这里返回类型依赖输入的 n，所以不能把它当成普通 JavaScript。递归也必须有终止依据：每次都减小自然数，最终到达 0。否则写一个永远调用自己的函数，声称它能返回任意命题的证明，整个对应就失去意义了。
从这个角度看，很多逻辑操作都变成了“类型体操”：找一个合适的构造，让要求的类型确实有对象。AI 擅长生成和修改程序，证明助手又提供严格反馈，两者自然就接到了一起。
这么好的东西为什么不早学？老师可以开玩笑说：“因为老师不会，也学不动了啊。”但有了 AI 的帮助，也许小学生都可以尝试这样的交互。真正变化的是学习入口：可以先提出一个小目标，让 AI 演示，自己观察每一步如何改变已知和目标，再逐渐建立理解。
课堂上还有一个“鬼故事”：老师烂尾的博士论文里留下过一个 conjecture，也就是猜想。重新借助模型推进这个问题之后，讲述它的心情变成了“好消息，没有晚节不保；坏消息，连 proof 也开始变成一种 tax”。
此前我们已经谈过 storytelling tax、engineering tax、formalization tax：一个想法要变成别人能理解的叙述、可以运行的系统、机器可处理的形式表达，都需要付出大量劳动。如果连证明也越来越能够由机器承担，那么曾经被看作“顶尖数学智慧”的工作，其稀缺性会发生什么变化？这里的“tax”表达的是对劳动成本变化的冲击感，并不是说证明从此没有价值。
在继续从主定理推出一些有用结论后，老师还让模型评价工作的投稿前景：课堂记录中，GPT-6 给出“PODC Yes”，Claude Opus 5.5 给出“PODC borderline”。值得关注的是，提出问题的经验与解决问题的信心，仍然来自 Computer Science 的训练。知道什么问题值得问、结果能继续推出什么，比等待模型吐出一段漂亮答案更有力量。
这种变化也有实际研究作为背景。Anthropic 与 Theorem 的合作报告称，使用模型为一百多个开源软件库在 RISC-V 汇编层面证明了安全性质。它提示我们，过去因人力成本过高而难以规模化的工作，正在获得新的实现途径。参见 LLMs are making formal software verification feasible at a much larger scale。
接下来的问题变得更加尖锐：怎样防止“证了个寂寞”？假如要求账户余额非负，模型却给所有操作都加上“原地不动”，确实可能很容易保持非负，却根本没有实现转账。或者它把需要证明的结论偷偷写进前提，后面的推导再严密，也没有回答原问题。
形式化本身也可以执行、也可以测试。我们可以用熟悉的例子运行规格，检查它允许和拒绝哪些行为；可以给错误实现构造反例，看看规格是否真的排除了它；可以继续核对抽象模型与真实实现的对应关系。证明助手检查的是形式系统内部的推导，人还需要借助这些反馈，确认形式化表达对应了原本的意图。
AI 时代的一个重要能力，是在一定程度上掌握自己无法独立完成的力量。去体验超出能力边界的事情，再把提出问题、审查关键步骤、组织反馈的能力变成自己的一部分。
如果证明可以更便宜地构造，软件交付的形态也可能变化：交付代码时，同时交付它满足某项策略的证明，接收方检查证明，再决定是否接受代码。这就是 proof-carrying code，携带证明的代码。
这个想法不是生成式 AI 时代才出现的。1996 年，Necula 和 Lee 的《Safe kernel extensions without run-time checking》就讨论了用携带证明的方式接纳安全的内核扩展，并获得 OSDI 最佳论文奖。到本课程的 2026 年，已经过去三十年。参见论文摘要与大会获奖记录。
它把一种责任分工做得很清楚：代码提供者承担构造证明的工作，接收者根据自己的安全策略检查证明。接收者不必因为“作者值得信任”或“模型看起来很厉害”就接受代码。如果 AI 改变了构造证明的成本，这种很早就存在的架构，便可能在更大范围内成为现实。
理解这些历史，也能让我们对动不动就 claim “SOTA” 保持一点幽默感。老师给它编了几个恶搞展开：State of Trivial Arrogance、Slop Optimized To Ascend、Science of Trivial Advances。值得追问的不是一个名次是否足够漂亮，而是工作到底解决了什么问题，与已有思想是什么关系，改变了哪一部分真实成本。
当然，There is no Silver Bullet。形式化的价值，依赖于我们能否用比实现更简洁、独立的方式表达“正确”。“所有数组访问都在合法范围内”是一条可以反复应用的规则；它不需要把程序的每一个实现细节重新抄写一遍。这样的性质特别适合交给验证系统。
但“我要一个领导满意的教务系统”，该怎样形式化？领导到底怎么想的？“我要一个用户满意的折叠屏关闭特效”，什么才叫自然、舒适、符合预期？可以记录帧率和延迟，却不能直接把它们等同于满意。自动形式化（autoformalization）要把自然语言意图转成形式表达，而有些意图尚未清楚到可以直接翻译，甚至要在体验原型后才逐渐形成。
因此，证明能力增强以后，问题会继续向前移动：从实现是否符合规格，移向规格是否符合意图。测试、原型和人的反馈不会因此失去作用，它们也在帮助我们决定究竟该证明什么。
最后留一个课堂上的“暴论”：人类，尤其是负责缓慢、审慎思考的 System II，也许可以被理解为一个最终由形式推理系统裁决的过程；不稳定之处来自把现实转成形式表达时的随机性，以及推理中的错误注入。如果 AI 能不断解决这些问题，再接上更长程的反馈，人类还剩下什么？老师把这个方向推到极端，开玩笑说，剩下就是“人类的灭亡”了。
这是用来挑战直觉的猜想，并非已经得到证明的认知理论或技术预言。它把本讲的问题留给我们：当构造程序、寻找证明都越来越容易时，谁来决定正确的含义，又用什么反馈确认，我们证明的确实是值得证明的事情？