形式证道
你以为测试通过就是没bug。测试只能证明bug的存在，不能证明bug的不存在——这之间的鸿沟，就是形式化方法要填的。但穷举所有状态？2^n会要你的命。
雾锁证道门
证道之门的门楣上刻着四个字："形式证道。"门后是一片灰雾——由无数条断裂的状态转移边构成，没有五官，只有声音。诺依曼老祖站在门侧，手里捧着一摞案卷。
诺依曼老祖
「你要证道，先过这一关——这五份案卷，测试都'通过'了。可它们都杀了人。你能找出'测试通过'和'没有bug'之间的鸿沟吗？」
状态爆炸之雾
「测试通过了——这四个字，是我最喜欢的笑话。赌一局：你找得出'测试通过却仍致命'的案例吗？我赌你找不全。」
测试vs验证反直觉挑战器
五份案卷下注 → 逐一翻账 → 测试vs验证的本质鸿沟
逻辑基石 · 蕴含之误
石径尽头是一面刻满真值表的石壁。诺依曼老祖指着其中一行："命题'如果P则Q'（P→Q），当P为假时，整个命题为真还是为假？"
诺依曼老祖
「'如果下雨则地湿'——没下雨，这句话为真还是为假？直觉告诉你'无所谓'。但逻辑不这么看。」
状态爆炸之雾
「猜'不确定'嘛。直觉不会骗你的——直觉就是我。你一旦信了直觉，我就住进来了。」
逻辑基石 · 蕴含真值表组装器
预测三选一 → 填真值表四行 → 量词应用 · 第一崩塌落定
补完 P→Q 的真值表（点击单元格填值）
量词应用：∀x∈N, x+1 > x 用哪个量词？
状态之海 · 模型检验原理
石壁裂开一道缝，里面是一片无边的状态之海——每个状态是一颗发光的节点，状态转移边把它们连成一张巨网。诺依曼老祖递给你一只计数器。
诺依曼老祖
「模型检验的核心：把系统所有可能状态都列出来，逐一检查你要的性质在每个状态下是否成立。三个布尔变量——有多少种状态？」
状态爆炸之雾
「8个。不多嘛。再加一个变量呢？再加一个呢？放心，你数得过来。」
状态空间指数爆炸追踪器
拖滑块调变量数 → 看状态数2^n膨胀 → 拖缓解策略看效果
状态空间膨胀曲线（2^n）
缓解策略（拖入查看效果）
时序之眼 · LTL与CTL
状态之海深处悬着一面分叉镜——镜中时间不是一条线，而是一棵不断分叉的树。诺依曼老祖指着镜面。
诺依曼老祖
「你想验证'请求最终被响应'。但'最终'是什么意思？在每一条可能的路径上都被响应？还是存在至少一条路径上被响应？自然语言的'最终'，在逻辑里有两个截然不同的意思。」
状态爆炸之雾
「说'最终'就行了，别较真。模糊的规格，就是我的栖息地。」
LTL与CTL时序逻辑公式组装器
切LTL/CTL模式 → 拖算子组装公式 → 看路径验证结果
LTL公式：在每条路径上，请求后总会响应
路径语义验证
工具绑定
验证法器 · SPIN与NuSMV
石径前方是一座法器阁，阁中悬着两台巨大的机器——一台刻着"SPIN"，一台刻着"NuSMV"。诺依曼老祖递来一张模型卷轴。
诺依曼老祖
「互斥协议——两个进程争夺一个资源，不能同时进入临界区。用SPIN验证它。SPIN用LTL，NuSMV用CTL——S3你写的公式，工具替你跑。」
状态爆炸之雾
「工具？好。让它跑。跑完所有状态——你就'证明'了。你一定觉得，穷举到底就等于证明了吧？」
SPIN与NuSMV验证工具台
切工具标签 → 补完代码模板 → 运行验证 → FDIV缺陷复盘
SPIN · 互斥协议验证
[] (p1.cs == false -> <> p1.cs == true)
FDIV缺陷复盘（Pentium FDIV bug · 1994）
点击单元格——哪些除法对被工具标红？
Intel耗资4.75亿美元召回。测试漏了——因为测试只采样了部分输入。形式化验证能覆盖所有输入。
状态爆炸 · 穷举之极限
法器阁深处是一台巨大的推杆计数器，刻度从1到100。状态爆炸之雾盘在计数器上，声音甜得发腻。
状态爆炸之雾
「S2你亲手数过——3个变量8个状态，'不多'。加到10个呢？1024。工具跑得快，多加几个怕什么？推满它。推到100。」
诺依曼老祖
「我没有阻止你。我只是退后一步，看着你。」
状态爆炸推杆 · 2^n物理极限
推滑块到100变量 → 看状态数越过宇宙原子数 → 拖缓解策略 · 第二崩塌
证明之塔 · 定理证明方法
石壁崩塌处露出一座金色的塔——证明之塔。塔身由一节节金链构成，每一节是一个推理步骤。诺依曼老祖推开塔门。
诺依曼老祖
「模型检验是'走遍每条路'。定理证明是'证明所有路都通向同一个结论'——不用走，用逻辑推。Coq和Lean是证明之塔的法器。」
证明之塔 · Coq证明构造器
拖推理规则补完证明链 → Coq终端逐条运行 → 四色定理脉络
证明链：∀ n∈N, n+1 > n
Coq交互终端
Hoare之秤 · 程序正确性证明
证明之塔顶层悬着一架天平——Hoare之秤。左盘是前置条件P，右盘是后置条件Q，中间是程序S。诺依曼老祖指着天平中央的裂缝。
诺依曼老祖
「Hoare三元组 {P} S {Q}——如果执行前P成立，执行后Q成立。但程序有循环。循环的每一圈，你得找一个'不变式'——一个在循环开始前、每一圈结束后都成立的性质。找到它，证明之伤就愈合。」
状态爆炸之雾
「不变式？循环跑100万圈你也要证100万次吗？——你要是不找不变式，就回去遍历吧。」
Hoare与Curry-Howard推导组装器
看Hoare三元组 → 选正确不变式 → 验证三条件 → 证明之伤愈合
选择循环不变式 I（循环每一圈都成立的性质）
证明之伤 · 裂缝
S1的裂缝：直觉推理≠形式推理。不变式不是遍历——是证明。
找到正确的不变式，裂缝愈合。
类型即证明 · Curry-Howard与可计算性
Hoare之秤愈合处，两面镜子从虚空中浮现——左镜刻满命题，右镜刻满类型。它们的镜像内容，竟然一模一样。诺依曼老祖推开双镜。
诺依曼老祖
「你看这两面镜子——左边是命题，右边是类型。它们长得一样，因为它们就是同一个东西。这就是Curry-Howard对应。你写的每一行带类型的代码，都是一个证明的碎片。」
Curry-Howard对应与停机问题推导
配对命题↔类型 → 依赖类型证明 → 停机问题矛盾推导
配对：命题 ↔ 类型（点击配对）
依赖类型编辑器（Lean风格）
停机问题矛盾推导（点击展开每一步）
Boss 战 · 状态爆炸之雾三问
回廊灯火齐灭。灰雾从四面八方压过来，凝成一张巨大的、没有五官的脸——由无数条断裂的状态转移边构成。
状态爆炸之雾
「我是状态爆炸之雾。我不住在错误里——错误救不了我。我住在你'穷举就能证明一切'的傲慢里。你每以为遍历到底就等于证明，我就胖了一圈。三问。答错一题，雾就厚一分。」
渊账累计 0 笔 · 三问全对后清零
尾声 · 形式证道
雾散尽时证道门灯火重明，你手里的证明之链微微发光——不是它变回了原样，是它带着所有崩塌与愈合的痕迹，成了另一种完整。诺依曼老祖走过来，却没恭喜你。
诺依曼老祖
「你证道了。不是因为你答对了三问——答对的会忘。是因为你走过的每一次崩塌、每一次愈合，都刻在你手上了。但——你证明的是经典程序。量子程序的叠加态怎么验证？AI黑箱的决策路径怎么证明？并发无限状态系统的不变式怎么找？那里穷举不行，证明也不一定行。去ch26看看吧。」
知识图谱点亮 · 形式证道之悟
点亮全章8块碎片 → 证明链剪影定格 → 境界突破