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

待复核

是什么

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

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

你写一份”协议应该这样跑”的剧本（lamport-tla-1994：初始条件 Init，加上”每一步都按 Next 走”的时序公式）
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+ 含集合论，状态可以无限。TLC 只吃”有限状态、机器能求值”的规范；更抽象的证明留给后来的 TLAPS。取舍：自动化换表达力。
边走边查，先找最短错。不是先建整张状态图再查，而是生成一个状态就立刻核对（on-the-fly）。安全属性用 BFS，保证反例最短；活性检查再切到 DFS 找环。
用指纹当身份证。每个状态压成 64 位 fingerprint（论文原文），集合放内存、待查队列可落盘。碰撞概率约 2^-64 量级，极大状态空间时需留意；可用不同 -fp seed 重跑确认。这一招让 TLC 能扛亿级状态。
多线程 + 多机器。多个 worker 并行探索状态空间，磁盘与内存分工扛规模。1999 年这已是少见的”分布式模型检查器”。

实践案例

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

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

把这文件喂给 TLC（真实用法还要一份 .cfg 声明 Init/Next/Inv；这里用 tlc Counter.tla 作示意）。TLC 从 x=0 起按 Next 走到 x=5，逐步查 Inv，全过则报 No error has been found。

案例 2：TLC 怎么找到 race

写两进程互斥规范，把 Mutex == ¬(pc1 = "crit" ∧ pc2 = "crit") 设为不变量，但故意漏掉一个临界条件。TLC 很快吐出：

Error: Invariant Mutex is violated.
State 1: pc1="idle",   pc2="idle"     # 都空闲
State 2: pc1="trying", pc2="idle"     # P1 申请
...
State 6: pc1="crit",   pc2="trying"   # 还安全
State 7: pc1="crit",   pc2="crit"     # 同时进临界区 ← 违规

第 7 步才爆，根因往往在更早漏写的守卫；按迹回补条件即可。

案例 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 焦虑。指纹是 64 位，碰撞概率极低但仍非零。关键跑可换 -fp seed 重跑，看状态数是否一致。
反例迹很长但根因在前几步。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 —— 同样是”机器替你做严格推导”的思想，但作用域是类型而非时序

反向链接

dafny-2010 —— Dafny — 把”代码该满足的条件”直接写进语法，编译器自动证明
disel-2018 —— Disel — 把分布式协议拆成可独立证明、可拼装的 Coq 模块
ironfleet-2015 —— IronFleet — 把分布式协议证到一行 bug 都没有
verdi-2015 —— Verdi — 在 Coq 里完整证明 Raft 协议的分布式系统验证框架