TLC — 让 TLA+ 规范可以一键机检的模型检查器

是什么

TLC（TLA+ Checker）是 1999 年 Yu、Manolios、Lamport 三人写的一个模型检查器——你给它一份 TLA+ 写的系统规范，它把所有可能的执行路径机械地走一遍，每走一步都核对你写的安全规则。

日常类比：TLC 像一个不知疲倦的审稿实习生。

你写一份”协议应该这样跑”的剧本（lamport-tla-1994 里的 TLA+ 公式 Init ∧ □[Next]_v）
TLC 拿着剧本，把所有可能的演员走位都演一遍——A 先 B 后、A B 同时、A 卡住 B 接管……
每一帧都核对：“此刻有没有违反 Mutex 这条规则？”
一旦违反，吐出反例迹：从开机到崩溃的完整状态序列

人脑能想到 5 步深的 race，TLC 能找到 35 步深的。

为什么重要

不理解 TLC 没法解释的事：

AWS 凭什么敢说 DynamoDB / S3 上线前”穷举过所有竞态”？答：他们写 TLA+ 规范，跑 TLC（Newcombe 等 CACM 2015）
为什么 lamport-tla-1994 那篇论文里的 TLA 逻辑等了 5 年才在工业界开始有人听说？因为 1994 只有理论，1999 这篇 TLC 工具出来才让规范”可执行”
为什么 TLA+ 比同时期的 CSP / Z notation 更落地？关键就是有 TLC——纸面规范不能跑，工程师不会买账
MongoDB 副本集、Azure Cosmos DB 一致性、Intel 缓存协议、Elasticsearch 选主——背后都站着 TLC

一句话：1994 给了 TLA 这套数学语言，1999 给了它一个”按下回车就能跑”的引擎。

核心要点

TLC 的设计哲学可拆四点：

只跑 TLA+ 的可计算子集。完整 TLA+ 含集合论，理论上无限。TLC 限定到”有限状态、可机器求值的谓词”，把不能跑的部分留给定理证明工具 TLAPS。取舍：自动化换表达力。
on-the-fly + BFS。状态边生成边检查，不是先建好整张图再查。BFS 保证找到的反例最短（debug 友好）。活性检查切到 DFS 找环。
fingerprint 哈希存状态。每个状态用 128 位 hash 当身份证，集合放内存、状态队列放磁盘。代价是理论上有 2^-128 的 collision 假阴概率（实际从未踩到）。这一招让 TLC 能扛亿级状态空间。
多线程 + 多机器。worker 并发探索状态空间，状态集群锁守规模。TLC 是当年少见的”分布式模型检查器”。

实践案例

案例 1：跑通一个最小的 TLC

---- MODULE Counter ----
VARIABLE x
Init == x = 0
Next == x' = x + 1 /\ x < 5
Spec == Init /\ [][Next]_x
Inv  == x >= 0
====

把这文件喂给 TLC，命令：tlc Counter.tla。TLC 从 x=0 开始，按 Next 枚举到 x=5 停。对每个状态查 Inv，全过则报 No error has been found。

案例 2：TLC 怎么找到 race

写一份两进程互斥的 TLA+，故意把 Mutex == ¬(pc1 = "crit" ∧ pc2 = "crit") 设成检查目标，规范里漏掉一个临界条件。TLC 一秒内吐出：

Error: Invariant Mutex is violated.
State 1: pc1 = "idle", pc2 = "idle", turn = 1
State 2: pc1 = "trying", ...
...
State 7: pc1 = "crit", pc2 = "crit"  <-- 同时进临界区

七步反例，工程师按这个序列回去补条件即可。

案例 3：AWS 真实战绩

Newcombe 等 CACM 2015 报告：

DynamoDB 团队写 ~1000 行 TLA+ 规范，TLC 跑出 35 步深的并发 bug——纸面 review 永远走不到
S3 用 TLA+ 规范了一致性协议，TLC 抓到一个工程师以为不可能的死锁
工程师反馈：“TLA+/TLC 让我们敢做激进优化”——确认无 race 后才放手改

案例 4：状态空间爆炸的实操

写 5 节点 Paxos，参数全开，TLC 状态数会冲到 10^9 量级，单机几小时跑不完。常用对策：

对称约简：声明 Servers 是对称集合，TLC 只探索一种排列
约束状态：加 StateConstraint == Len(msgs) <= 3 限制消息缓冲
分布式跑：开 8 台机器，TLC 自动分片

踩过的坑

把 TLA+ 当代码写。TLC 报错”can’t evaluate”通常是你写了不可机检的高阶逻辑。规范不是程序，要写得”小且抽象”。
状态空间爆炸。新人第一次跑 5 节点协议会卡死。先用 2 节点跑通再扩，永远先做对称约简。
公平性配错。检查活性时弱公平（WF）和强公平（SF）含义不同。WF：动作连续可发就一定发；SF：无限次可发就一定发。选错让 liveness 假阴/假阳。
fingerprint collision 焦虑。理论 2^-128，实际可忽略。关键系统真担心，可以换更长 hash 或重跑确认。
反例迹很长但根因在前几步。TLC 给出 35 步反例时，bug 通常在第 3-5 步，后面都是连锁。要会读迹、抓首发分歧。

适用 vs 不适用场景

适用：

分布式协议（共识、复制、租约、事务）—— 主战场
并发数据结构（无锁队列、读写锁）正确性
缓存一致性、内存一致性模型
设计审查阶段需要”机器穷举所有交错”才放心的关键系统

不适用：

算法效率分析（TLC 不管时间复杂度）
数值/概率系统（要 PRISM 这类概率检查器）
状态空间天文级又不需要严密保证的 UI / 业务逻辑
完全无形式化背景的团队（学习曲线 2-4 周起步）

历史小故事（可跳过）

1977 年：Pnueli 把时序逻辑引入 CS（图灵奖工作之一）
1989 年：SPIN 模型检查器问世，输入是 Promela，验证电信协议起家
1994 年：Lamport TOPLAS 发表 TLA 逻辑（lamport-tla-1994）——但只有理论，没工具
1999 年：本论文 CHARME 发表，Yu-Manolios-Lamport 写出 TLC，TLA+ 工具链开端；同年 biere-bmc-1999 发表 BMC，是另一条 SAT 风格的模型检查路线
2002 年：Lamport 出书《Specifying Systems》，定义 TLA+ 完整语法
2014–2015 年：Newcombe 在 AWS 把 TLA+/TLC 推向工业主流，CACM 文章引爆
2019 年起：Apalache 用 SMT 做符号 model checking，把 TLA+ 推到更大规模

Manolios 后来去了 Northeastern，做 ACL2 定理证明；Yu 在 Microsoft Research 继续做工具；Lamport 2013 拿图灵奖，TLA+ 是奖词关键贡献之一。

学到什么

理论 → 工具，工业才会用：1994 年 TLA 论文学界没多少人读，1999 年 TLC 出来才让 TLA+ 落地。光有逻辑不够，要能”按一下就跑”
限制是工具的力量：TLC 砍掉一半 TLA+（高阶逻辑、无限集合）才换来自动化。取舍是工程美德
fingerprint hash 这种工程 trick 决定生死：换成全状态存储 TLC 就处理不了亿级空间，工程层面的小决定改变工具能力上限
形式化方法的工业落地需要 30 年耐心：Pnueli 1977 → Lamport 1994 → TLC 1999 → AWS 2014——每步都不是轰动，但累计起来重塑了分布式系统设计审查

关联

lamport-tla-1994 —— TLA 逻辑理论；本文是这套理论的”可执行引擎”
lamport-1978 —— Lamport 分布式时序观的起点；TLA+ 是这条思想的延续
biere-bmc-1999 —— 同年的 Bounded Model Checking；TLC 显式状态、BMC 用 SAT 符号化，互为对照
paxos-1998 —— Paxos 共识协议；TLA+/TLC 的经典验证对象
hoare-logic —— 另一条”程序正确性 = 逻辑命题”流派；Hoare 是演绎、TLC 是穷举
hindley-milner —— 同样是”机器替你做严格推导”的思想，但作用域是类型而非时序

反向链接

biere-bmc-1999 —— Bounded Model Checking — 把硬件验证翻译成一道 SAT 题
dafny-2010 —— Dafny — 把”代码该满足的条件”直接写进语法，编译器自动证明
disel-2018 —— Disel — 把分布式协议拆成可独立证明、可拼装的 Coq 模块
hindley-milner —— Hindley-Milner — 编译器自己猜变量类型
hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
ironfleet-2015 —— IronFleet — 把分布式协议证到一行 bug 都没有
lamport-1978 —— Lamport 1978 — 分布式系统里没有”绝对的同时”
lamport-tla-1994 —— TLA — 把状态机和时序逻辑捏成一个公式
paxos-1998 —— Paxos 1998 — 古希腊议会寓言里藏的共识协议
verdi-2015 —— Verdi — 在 Coq 里完整证明 Raft 协议的分布式系统验证框架