形式化验证与 TLA+：行为的数学建模

2015 年 4 月，AWS 的工程师在《Communications of the ACM》上发表了一篇论文¹，记录了 TLA+ 在 DynamoDB 复制协议中发现的一个极端 bug——它经过了设计审查、代码审查和大量测试，没有人发现它。TLC 模型检验器给出的最短反例轨迹包含 35 个高层步骤。论文指出：在足够大的规模下，这种复合事件的低概率并不能构成防御——历史上 AWS 在生产环境中确实观察过同等复杂的组合。

本文讨论的问题只有一个：怎样在代码落地之前，用数学方法证明一个系统设计没有逻辑错误。

一、测试的边界

先看一个简单的问题：一个全局计数器 counter，两个线程各自执行 100 次递增。最终 counter 的值是多少？

学过并发编程的人知道答案：不一定是 200。counter += 1 不是原子操作——它包含读、加、写三步。两个线程同时读到同一个值，各自加 1 后写回，结果相当于丢失了一次递增。

这是并发编程中最基础的竞态条件。常规对策是加锁、用原子指令、或者按并发模型重新设计。

但这里有一个更根本的问题：你怎么确认你的对策是正确的？

测试可以让你更自信，但无法穷举。两个线程各执行 100 步——不考虑更复杂的交错，仅指令级的交错组合就已经是天文数字。线程数更多、步骤稍复杂之后，状态空间急剧膨胀，任何基于采样的验证手段都碰不到边界。

这不是测试方法论的问题，也不是工程师不够认真。这是一个组合数学问题：

系统的状态空间随并发组件的数量呈指数增长——这叫状态空间爆炸（state space explosion）。

2015 年，Kyle Kingsbury 在 Jepsen 分布式系统正确性分析中对 MongoDB 的复制协议进行了系统性测试²。当时 MongoDB 使用的复制协议（protocol v0）以 wall-clock 时间戳作为操作排序的依据。在时钟偏斜的网络分区场景下，一个被隔离的节点如果时钟较快，可能在选举中胜出，导致已经被多数派确认的写入被静默丢弃。Jepsen 的测试显示：在 4525 次以 majority write concern 提交的写入中，有 93 次被确认后丢失。这不是一个可以通过增加测试用例数量来解决的问题——它是协议设计的逻辑缺陷。

另一个更著名的案例是 Therac-25 放射治疗机事故（1985-1986）³：软件中的竞态条件导致 6 名患者接受了超过百倍剂量的辐射，其中 3 人死亡。事后调查发现，触发条件依赖于操作员在特定时间窗口内按下特定按键组合——在测试期间从未被复现。

这些事故有一个共同特征：不是代码写错了，是设计本身存在逻辑漏洞。代码忠实地执行了设计，但设计没有覆盖所有可能的状态交错。

形式化验证要解决的就是这个问题。

二、形式化验证：用数学描述行为

2.1 定义

形式化验证（formal verification）是指用数学语言严格描述一个系统的行为规范（specification），然后通过数学证明或穷举搜索，验证系统的行为是否满足规范。

拆成两步理解：

1. 写规范（specification）：用精确的数学语言定义「什么行为是合法的」。
2. 做验证（verification）：检查系统的所有可能执行路径是否都满足这个规范。

这与测试有本质区别。测试只能检查有限个具体执行路径。形式化验证检查所有路径。

2.2 安全性与活性

形式化验证中，属性分为两类。这个分类来自 Leslie Lamport 在 1977 年的一篇论文。

安全性（Safety）：坏事永远不会发生。

Lamport 给过一个精辟的表述——safety properties 意味着「something bad never happens」。更形式化地说，如果某个属性在一次执行的每一个有限前缀中都成立，那么它在整次执行中也成立。

典型的安全性属性：

• 互斥：两个进程不可能同时进入临界区
• 不变量（invariant）：账户总金额在任意时刻都等于初始总额
• 无死锁：不存在一组相互等待的进程
• 类型一致：某个变量在所有可达状态中的取值都在合法范围内

活性（Liveness）：好事最终一定会发生。

活性描述的是进展——系统不会永远卡住。典型例子：

• 每个请求最终都会收到响应
• 如果某个进程请求进入临界区，它最终会进入
• 网络分区恢复后，节点最终会达成一致

一个常见误区是把安全性和活性对立起来。它们不是对立的，而是正交的。一个正确的系统需要同时满足两类属性。

2.3 两种路线：模型检验与定理证明

形式化验证有两条技术路线，各自适合不同的场景。

模型检验（Model Checking）：穷举系统的所有可达状态，逐一检查每个状态是否满足给定属性。

• 优点：全自动，发现有问题的状态时能给出具体的反例路径
• 缺点：受状态空间大小限制，无法处理无限状态系统
• 代表工具：TLC（TLA+ 的模型检验器）、Spin、NuSMV

定理证明（Theorem Proving）：将系统和属性编码为数学命题，然后构造一个机器可检查的证明。

• 优点：可以处理无限状态系统
• 缺点：需要大量的人工引导，门槛高
• 代表工具：Coq、Isabelle/HOL、TLAPS（TLA+ 的证明系统）

实践中，绝大多数工程场景用模型检验就足够了。TLA+ 的定位也是以模型检验为主，辅以定理证明作为补充。

2.4 状态机：共同的数学模型

模型检验和定理证明都依赖于同一个底层模型：状态机。

一个并发系统可以抽象为：

• 一组变量（状态）
• 一组动作（状态转移规则）
• 一组初始状态
• 一组需要满足的属性

状态机构成了一个有向图：节点是状态，边是动作。形式化验证就是在这张图上做穷举搜索。

初始状态 ──→ 状态1 ──→ 状态3 ──→ ...
  │                      │
  └──→ 状态2 ────────────┘

这个模型足够通用：操作系统中的进程调度、分布式系统中的共识协议、SoC 中的总线仲裁——都可以编码为状态机。

三、TLA+ 的核心设计

3.1 背景

TLA+（Temporal Logic of Actions）由 Leslie Lamport 设计。Lamport 是图灵奖得主，LaTeX 的作者，Paxos 协议的发明者，也是安全性和活性理论框架的提出者。

TLA+ 的定位非常明确：描述并发和分布式系统的行为，而不是描述程序的执行过程。它是一个规范语言，不是编程语言。这一点直接影响了很多设计决策——没有类型系统，没有函数式抽象，甚至连 if-then-else 的语义都和常规语言不同。

3.2 时序逻辑：一个直观解释

TLA+ 的数学基础是 Lamport 自己提出的行为逻辑（Temporal Logic of Actions, TLA）。TLA 融合了动作逻辑和时序算子——使用了和线性时序逻辑（LTL）类似的 $\Box$、$\Diamond$ 算子，但语义不同：TLA 的核心创新是「动作」（action）概念，把状态转移和时序逻辑统一在同一个框架中。

先看两个核心算子。

Always / 总是（$\Box$）：$\Box P$ 表示 $P$ 在执行的每一步都成立。

• $\Box(balance \ge 0)$ —— 余额始终不为负。

Eventually / 最终（$\Diamond$）：$\Diamond P$ 表示 $P$ 在未来的某个时刻会成立。

• $\Diamond(response\_sent = \text{TRUE})$ —— 响应最终会被发出。

用这两个算子可以表达常见的系统属性：

• $\Box\Diamond(progress = \text{TRUE})$ —— 经常有进展（弱公平性的一种表述）
• $\Diamond\Box(terminated = \text{TRUE})$ —— 最终永久停留在终止状态

TLA+ 中频繁出现的符号不多，下面是本文涉及的核心记号。

$\Box$ 和 $\Diamond$ 是印刷形式。在 .tla 源文件中使用 ASCII 写法：[] 对应 $\Box$，<> 对应 $\Diamond$。

TLA+ 的创新在于，它把时序逻辑和状态转移统一在同一个框架中。Lamport 管这个叫「行为的数学」（The Mathematics of Behaviors）。一个行为（behavior）就是状态的无限序列：

系统的规范是一个谓词，它断言某个行为是否合法。一个规范可能允许多个行为——非确定性是被鼓励的，因为规范应该说清楚「什么是必须的」，而不该规定「该以什么顺序执行」。

3.3 动作与不变量

在 TLA+ 中：

• 动作（Action）：一个包含初始状态变量和下一状态变量（带 ' 后缀）的谓词。例如 x' = x + 1 是一个动作，描述变量 x 递增 1。
• 不变式（Invariant）：一个仅涉及当前状态变量的谓词，必须在每一步都成立。例如 x ≥ 0。
• 时序属性（Temporal Property）：涉及 $\Box$ 或 $\Diamond$ 算子的公式，描述跨步骤的约束。

TLA+ 的公式中，同一个变量名不带 ' 表示当前状态的值，带 ' 表示下一状态的值。这个约定来自 Lamport 的另一个观察——在数学中，变量不是一个会变化的存储位置，而是一个值。但在状态转移中，同一个变量在不同状态中有不同的值。加 ' 是一种简洁的标记方式，避免引入额外的语法。

3.4 PlusCal：另一种入口

纯 TLA+ 使用数学公式描述系统，对习惯了 C 风格语法的程序员不够友好。PlusCal 是 Lamport 设计的另一种语法，长得像 Pascal 或玩具版的 C，但语义完全等价于 TLA+——PlusCal 代码会被翻译为 TLA+ 公式，然后再交给 TLC 检验。

一个 PlusCal 版本的计数器递增（两个并发进程，各自循环递增）：

---- MODULE Counter ----
EXTENDS Naturals, TLC

(* --algorithm Counter {
    variable counter = 0;

    process (P \in {1, 2}) {
        inc:
            counter := counter + 1;
            goto inc;
    }
} *)
====

process (P \in {1, 2}) 声明了两个进程，P 是进程标识。翻译后，每个标签（inc:）对应一个由 pc 变量控制的状态转移，翻译器自动处理交错语义——每一步只执行一个进程的一个标签。

PlusCal 适合描述控制流复杂的算法。但本文接下来的实战案例——并发转账——控制流极简单（两个进程各一两步），复杂的是状态变量和不变量的交互。在这种情况下，直接用纯 TLA+ 写反而更短、更透明：你能看到每一个状态转移的前置条件和效果，TLC 报错时变量轨迹也直接对应你定义的变量名，不需要绕过翻译层去理解自动生成的 pc 变量。

接下来的实战全部使用纯 TLA+。

四、建模实战：用 TLC 检验并发转账

这一节不再使用示意性的伪代码。下面每一步都在本地 TLA+ 环境中实际执行，输出直接来自 TLC。

工具是单个 jar 包，命令行模式：

# 运行 TLC 模型检验
java -cp tla2tools.jar tlc2.TLC Spec.tla

如果用 PlusCal 写规范，还需要先用 pcal.trans 翻译为 TLA+；第四节实战全部使用纯 TLA+，不需要这一步。PlusCal 翻译器的用法见第七节。

4.1 问题

两个账户 alice 和 bob，初始各 100。两个并发操作：

• A：从 alice 转 30 给 bob
• B：从 bob 转 40 给 alice

期望的安全性属性：任意时刻 alice + bob = 200。

4.2 原子版本：不变量始终成立

先将每个转账建模为一步原子操作——扣款和入账在同一个 TLA+ 动作（action）中完成。文件 TransferAtomic.tla：

---- MODULE TransferAtomic ----
EXTENDS Naturals, TLC

CONSTANTS AMOUNT_A, AMOUNT_B

VARIABLES alice, bob, a_done, b_done

vars == << alice, bob, a_done, b_done >>

Init ==
    /\ alice  = 100
    /\ bob    = 100
    /\ a_done = FALSE
    /\ b_done = FALSE

TotalInvariant == alice + bob = 200

A_transfer ==
    /\ ~a_done
    /\ alice >= AMOUNT_A
    /\ alice'  = alice - AMOUNT_A
    /\ bob'    = bob   + AMOUNT_A
    /\ a_done' = TRUE
    /\ b_done' = b_done

A_skip ==
    /\ ~a_done
    /\ alice < AMOUNT_A
    /\ a_done' = TRUE
    /\ UNCHANGED << alice, bob, b_done >>

B_transfer ==
    /\ ~b_done
    /\ bob >= AMOUNT_B
    /\ bob'    = bob   - AMOUNT_B
    /\ alice'  = alice + AMOUNT_B
    /\ b_done' = TRUE
    /\ a_done' = a_done

B_skip ==
    /\ ~b_done
    /\ bob < AMOUNT_B
    /\ b_done' = TRUE
    /\ UNCHANGED << alice, bob, a_done >>

Terminating ==
    /\ a_done
    /\ b_done
    /\ UNCHANGED vars

Next ==
    \/ A_transfer
    \/ A_skip
    \/ B_transfer
    \/ B_skip
    \/ Terminating

Spec == Init /\ [][Next]_vars

====

完整文件：TransferAtomic.tla

每个动作的结构：前置条件（~a_done、余额检查）在前，状态转移（alice' = alice - AMOUNT_A）在后。A_skip 和 B_skip 处理余额不足时直接标记完成的退化情况——本例中 alice 初始 100、bob 初始 100，金额分别为 30 和 40，余额检查总是通过，所以 A_skip/B_skip 实际不会被触发；但把它们写进 Next 能保证模型在任意参数下都不会因为「没有匹配的动作」而误报死锁。Terminating 在两个操作都完成后允许系统无限口吃——TLC 需要所有可达状态都存在合法的下一步，否则报告死锁。

配置文件 TransferAtomic.cfg：

SPECIFICATION Spec
CONSTANT
    AMOUNT_A = 30
    AMOUNT_B = 40
INVARIANT
    TotalInvariant

运行 TLC：

java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC -nowarning TransferAtomic.tla

输出：

Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable
  states because two distinct states had the same fingerprint:
  calculated (optimistic): val = 4.3E-19
6 states generated, 4 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.

全部 4 个可达状态均满足 TotalInvariant。

4.3 拆开两步：让 TLC 找到 bug

去掉原子性假设。将每次转账拆为两个独立动作：扣款 + 入账。文件 TransferNonAtomic.tla：

---- MODULE TransferNonAtomic ----
EXTENDS Naturals, TLC

CONSTANTS AMOUNT_A, AMOUNT_B

VARIABLES alice, bob, a_step, b_step

vars == << alice, bob, a_step, b_step >>

Init ==
    /\ alice  = 100
    /\ bob    = 100
    /\ a_step = "idle"
    /\ b_step = "idle"

TotalInvariant == alice + bob = 200

A_step1 ==
    /\ a_step = "idle"
    /\ alice >= AMOUNT_A
    /\ alice'  = alice - AMOUNT_A
    /\ bob'    = bob
    /\ a_step' = "credited"
    /\ UNCHANGED b_step

A_step1_skip ==
    /\ a_step = "idle"
    /\ alice < AMOUNT_A
    /\ a_step' = "done"
    /\ UNCHANGED << alice, bob, b_step >>

A_step2 ==
    /\ a_step = "credited"
    /\ alice'  = alice
    /\ bob'    = bob + AMOUNT_A
    /\ a_step' = "done"
    /\ UNCHANGED b_step

B_step1 ==
    /\ b_step = "idle"
    /\ bob >= AMOUNT_B
    /\ bob'    = bob - AMOUNT_B
    /\ alice'  = alice
    /\ b_step' = "credited"
    /\ UNCHANGED a_step

B_step1_skip ==
    /\ b_step = "idle"
    /\ bob < AMOUNT_B
    /\ b_step' = "done"
    /\ UNCHANGED << alice, bob, a_step >>

B_step2 ==
    /\ b_step = "credited"
    /\ bob'    = bob
    /\ alice'  = alice + AMOUNT_B
    /\ b_step' = "done"
    /\ UNCHANGED a_step

Terminating ==
    /\ a_step = "done"
    /\ b_step = "done"
    /\ UNCHANGED vars

Next ==
    \/ A_step1
    \/ A_step1_skip
    \/ A_step2
    \/ B_step1
    \/ B_step1_skip
    \/ B_step2
    \/ Terminating

Spec == Init /\ [][Next]_vars

====

完整文件：TransferNonAtomic.tla

与原子版本相比，每个原子的 A_transfer 被拆成了 A_step1（扣 alice）和 A_step2（入 bob），中间插入一个状态 a_step = "credited" 表示「已扣款、未入账」。A_step1_skip 对应原子版本的 A_skip——余额不足时直接标记 done，跳过扣款；B_step1_skip 同理。B 的结构与 A 完全对称。

配置文件不变，运行 TLC：

java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC -nowarning TransferNonAtomic.tla

输出：

Error: Invariant TotalInvariant is violated.
Error: The behavior up to this point is:

State 1: <Initial predicate>
/\ b_step = "idle"
/\ alice  = 100
/\ a_step = "idle"
/\ bob    = 100

State 2: <A_step1 line 30, col 5 to line 35, col 23 of module TransferNonAtomic>
/\ b_step = "idle"
/\ alice  = 70
/\ a_step = "credited"
/\ bob    = 100

2 states generated, 2 distinct states found, 0 states left on queue.

TLC 在 State 2 就捕获到违规。A_step1 执行后 alice 已被扣款（70），但 A_step2 尚未将 30 转入 bob。此刻 alice + bob = 170 ≠ 200。

关于输出中的行号：line 30, col 5 to line 35, col 23 指的是 TransferNonAtomic.tla 文件中的第 30–35 行（即 A_step1 动作体），不是上方代码块在本文中的行号。读者可打开完整文件对照。

这就是模型检验的核心价值：不但告诉你不变量被违反了，还给出精确的反例路径——每一步的状态和触发动作。

4.4 修复：回到原子性

修复方式取决于你的设计决策。在本例中，将 A_step1 和 A_step2 合并为单个 A_transfer 动作（即 4.2 中的原子版本），TLC 验证通过。

这种拆分→暴露→修复→重新验证的循环，是使用 TLA+ 的标准工作流。它不是一次性证明「系统完全正确」，而是不断用模型检验冲击设计，直到找不到反例为止。

五、三个进阶概念

第四节展示了 TLA+ 的最小可用子集——变量、动作、不变量、Next 公式——已经足以发现并发设计中的逻辑漏洞。以下三个概念把这个子集扩展到真实系统的规模。

5.1 精炼（Refinement）

规范很少一步到位。通常先写一份高层的抽象规范——说清楚系统从外部看应该有什么行为，不关心内部细节。然后逐层向下细化数据结构、消息格式、故障处理。

精炼描述的是「下层规范实现了上层规范」这种关系。形式化定义：

规范 $S_2$ 精炼规范 $S_1$，当且仅当 $S_2$ 的每一个合法行为也是 $S_1$ 的合法行为。

精炼的关键作用是分层验证。如果 $S_2$ 精炼 $S_1$，并且 $S_1$ 满足某个属性 $P$，那么 $S_2$ 自动满足 $P$。这意味着可以在一份高层、易于验证的规范上证明关键属性，然后逐步细化，每步只验证精炼关系，而不用在最终那个充满实现细节的规范上直接证明。

5.2 口吃步（Stuttering Steps）

在 TLA+ 中，一个动作可以允许「什么都没变」——即 $x' = x$。这种步骤叫口吃步。第四节里那个 Terminating 动作就是口吃步的实例，这里补充它的理论意义。

两个转账都完成后，系统已经没有有意义的行为可做，但 TLC 的死锁检查要求每个可达状态都存在合法的下一步——Terminating 用一个什么都不变的动作来满足这个要求，告诉 TLC「到此为止了，后面的步都是重复这个状态」。

这看起来多余，但在精炼关系中至关重要。上层规范可能允许一步完成一个操作，下层实现可能需要多步。如果禁止口吃步，精炼就不可行——下层多出的步骤在上层看来没有对应动作。允许口吃步之后，上层可以用口吃步「等待」下层的中间步骤完成，从而保证行为序列的对应关系。

Lamport 花了很多笔墨讨论这个点。他的核心思想是：规范语言应该在数学上方便，而不是在执行上方便。口吃步让精炼的数学定义变得干净。

5.3 公平性（Fairness）

模型检验中，「所有可能的路径」包含了那些进程永远不被调度的路径。这在真实系统中通常不会发生——调度器会给每个就绪进程机会。

弱公平性（weak fairness）要求：如果一个动作从某一步开始持续可用（enabled），那么它最终会被执行。

强公平性（strong fairness）要求更强：如果一个动作无限多次变为可用，那么它最终会被执行。

TLA+ 用 $\Box\Diamond$ 和 $\Diamond\Box$ 算子来精确表达公平性，它们是 TLA 公式的组成部分，不单独作为配置项。公平性约束对活性属性的验证至关重要——没有公平性约束，很多活性属性都无法被满足，因为规范允许调度器永远忽略某个进程。

六、工业界的两份实战报告

如果说第四节说明的是"小规模下 TLA+ 怎么用"，第五节的精炼、口吃步和公平性解决的是"怎样把这种能力扩展到真实系统"。以下两份报告证明，这条路已经走通了。

6.1 AWS：DynamoDB 复制协议

AWS 从 2011 年开始在系统设计中使用 TLA+。2012 年 1 月，一位工程师在 DynamoDB 的复制协议规范中发现了本文开头提到的那个 bug，整个过程记录在论文《How Amazon Web Services Uses Formal Methods》（Newcombe et al., 2015）中。

DynamoDB 使用多副本同步复制来保证数据不丢失。复制协议的核心是一个状态机（见 2.4 节），不同节点在正常流程、故障恢复和成员变更等场景下执行角色转换。正常流程不复杂，但在节点宕机、网络延迟、消息重传等异常组合下，状态机的边角情况急剧增多——这正是第一节所说的「状态空间爆炸」在真实系统中的体现。

AWS 团队先用 TLA+ 写了一份高层的协议规范，然后用 TLC 对一个小规模模型做穷举检验。TLC 找到了一个没有在任何测试用例中被覆盖的反例——该 bug 可能导致数据丢失，触发它需要一系列故障和恢复步骤以特定顺序与正常处理逻辑交错。论文记载，TLC 给出的最短反例轨迹包含 35 个高层步骤。这个 bug 在此之前通过了设计审查、代码审查和大量测试，负责该模块的工程师事后表示：即使投入更多精力做常规测试，也不可能发现它。

TLA+ 的价值不在于找到了这个特定 bug——而在于它证明了修复后的协议在所有可能的交错下都不会再违反该属性。测试可以增加信心，但给不了保证。

6.2 Xbox 360：内存一致性协议的隐蔽 bug

另一个经典案例来自微软。Xbox 360 使用 PowerPC 架构的 CPU，其弱内存模型允许读写操作被重排——这与 x86 的强内存模型有本质区别。为了保证正确性，开发者需要使用内存屏障指令（如 lwsync）来约束重排行为，但对这些规则的推理极其容易出错。和第一节的多线程交错一样，这里的困难在于：人类很难穷举所有可能的重排组合，而一个遗漏的路径就可能导致系统进入非法状态。

微软工程师 Chuck Thacker 和一名实习生在为 Xbox 360 编写内存一致性协议的 TLA+ 规范时，模型检验发现了一个关键的硬件 bug——该 bug 一旦进入量产，将导致任何一台 Xbox 360 在使用约 4 小时后必然崩溃。硬件制造商（IBM）最初回复「系统不可能进入此状态」，工程师随后用 TLA+ 模型给出了一条精确的行为轨迹，证明了该状态确实可达。

这个案例展示的不是"事后证明正确"，而是写规范的过程本身就能暴露设计缺陷。Lamport 在 2014 年的演讲「Thinking for Programmers」⁴ 中专门讲述了这个故事，说明当你被迫用数学语言精确描述一个系统的行为时，很多被模糊自然语言掩盖的问题会自然浮现。

七、工具链与学习资源

TLA+ 生态围绕一个 jar 包构建。所有工具共享同一个 classpath，命令行是核心操作方式。IDE 和 VSCode 扩展只是它的 UI 封装——理解 CLI 之后再使用它们事半功倍。

本节是复现第四节案例所需的工具参考。初次阅读可只看 7.1（获取 jar 包）和 7.3 前半段（TLC 基本用法），其余按需查阅。

7.1 获取与安装

从 TLA+ 官方 GitHub 下载 tla2tools.jar。安装就是下载这个 jar 文件，不需要编译、不需要 Maven。

建议在 shell 配置中加上别名：

alias tlc='java -XX:+UseParallelGC -cp /path/to/tla2tools.jar tlc2.TLC'
alias pcal='java -cp /path/to/tla2tools.jar pcal.trans'
alias sany='java -cp /path/to/tla2tools.jar tla2sany.SANY'

-XX:+UseParallelGC 不是必须的，但 TLC 在并发 GC 下吞吐量更好——没有这个参数 TLC 每次启动都会打印一条 warning。

7.2 pcal.trans —— PlusCal 翻译器

PlusCal 源码写在 .tla 文件中的 (* --algorithm ... *) 注释块内。pcal.trans 读取这个注释块，生成等价 TLA+ 公式，写回同一个文件。

基本用法：

java -cp tla2tools.jar pcal.trans Spec.tla

该命令将 Spec.tla 中的 PlusCal 算法翻译为标准 TLA+，可选生成配套的 .cfg 文件。翻译后的代码插入在原文件中 \* BEGIN TRANSLATION 和 \* END TRANSLATION 之间，位于模块结束符 ==== 之前。再次运行翻译器时会覆盖这一段，不会影响算法注释块以上的内容。

全部选项：

常用组合：

# 翻译并生成 Termination 属性配置
java -cp tla2tools.jar pcal.trans -termination Spec.tla

# 翻译但不生成 .cfg（适合已有手工配置的场景）
java -cp tla2tools.jar pcal.trans -nocfg Spec.tla

# 翻译并合取弱公平性
java -cp tla2tools.jar pcal.trans -wf Spec.tla

注意：pcal.trans 的 process 声明使用 process (P \in Set) 语法，if 采用 C 风格 if (condition) { ... }。详见 PlusCal 手册。

7.3 TLC —— 模型检验器与仿真器

TLC 是 TLA+ 生态的核心工具。两种运行模式：

模型检验模式（默认）：穷举搜索状态空间，验证指定属性。广度优先搜索，直到状态空间耗尽或找到反例。

仿真模式（-simulate）：随机采样执行路径。适合状态空间过大无法穷举的场景。

基本用法（模型检验）：

java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC Spec.tla

TLC 自动寻找与 .tla 同名的 .cfg 配置文件。如果 .cfg 文件名不同，用 -config 指定。

.cfg 配置文件语法

SPECIFICATION Spec          \* 必须：TLA+ 规范名称

CONSTANT                    \* 为模块中声明的 CONSTANT 赋值
    AMOUNT_A = 30
    AMOUNT_B = 40

INVARIANT TotalInvariant    \* 要检验的不变式（可多个，每行一个）
INVARIANT NoOverdraft

PROPERTY Termination        \* 要检验的时序属性

CHECK_DEADLOCK FALSE        \* 默认 TRUE，设为 FALSE 不检查死锁

CONSTRAINT C                \* 状态约束：只搜索满足 C 的状态
ACTION_CONSTRAINT A         \* 动作约束：只执行满足 A 的动作
VIEW V                      \* 视图：用 V 替换变量集合打印状态

常用选项（模型检验模式）

仿真模式选项（仅 -simulate 模式有效）：

使用示例：

# 仿真模式：随机采样 500 条 trace，深度 200
java -cp tla2tools.jar tlc2.TLC -simulate num=500 -depth 200 Spec.tla

解读 TLC 输出

模型检验通过（第四节原子版本的实际输出）：

Model checking completed. No error has been found.
6 states generated, 4 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.

• states generated：TLC 实际展开的状态总数（含重复访问）
• distinct states：去重后的独立状态数
• depth：状态图的深度（从初始状态到最深状态的最长路径长度）

模型检验失败（第四节非原子版本）：

Error: Invariant TotalInvariant is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ b_step = "idle"
/\ alice = 100
/\ a_step = "idle"
/\ bob = 100

State 2: <A_step1 line 30, col 5 to line 35, col 23 of module TransferNonAtomic>
/\ b_step = "idle"
/\ alice = 70
/\ a_step = "credited"
/\ bob = 100

TLC 给出从初始状态到违规状态的完整路径。每个状态列出所有变量的值，状态之间标注触发了哪个动作以及该动作在源文件中的位置（line 30, col 5）。

7.4 SANY —— 解析器与静态检查

SANY 是 TLA+ 的词法和语法分析器。单独运行它有两种用途：(1) 检查模块的语法和语义错误、缺失依赖、命名冲突，不执行模型检验；(2) 在写大型规范时快速验证模块结构，比跑 TLC 便宜得多。

java -cp tla2tools.jar tla2sany.SANY Spec.tla

输出示例（无错误时）：

****** SANY2 Version 2.1 created 24 February 2022
Parsing file Spec.tla
Semantic processing of module Spec

7.5 TLATeX —— 排版为 LaTeX / PDF

TLATeX 是 Lamport 写的排版工具，将 .tla 源文件转换为 .tex 文件，然后调用 latex（以及可选的 dvips）生成 PDF。它由 Lamport 基于 Dmitri Samborski 的想法实现——Lamport 恰好也是 LaTeX 的作者，所以这套工具链的每一个环节都出自同一个人之手。

依赖：系统必须安装 LaTeX（latex 命令）。生成 PDF 或 PostScript 还需 dvips 或 pdflatex。

基本用法：

java -cp tla2tools.jar tla2tex.TLA Spec.tla

输出文件包括 Spec.tex（LaTeX 源文件）、Spec.dvi（排版输出），如果指定了 -ps 还会生成 PostScript/PDF。

实际测试：第四节 TransferAtomic.tla 的排版结果如下——TLATeX 成功生成了 44538 字节的 .tex 文件（本机未安装 LaTeX，PDF 步骤无法完成，但不影响 .tex 的生成）：

tla2tex.TLA Version 1.0 created 12 Apr 2013
looking for file: TransferAtomic

常用选项：

实用示例：

# 带行号、12pt 字体的 PDF
java -cp tla2tools.jar tla2tex.TLA -number -ptSize 12 \
    -psCommand pdflatex -latexOutputExt pdf Spec.tla

# 注释配灰色底色，控制灰度
java -cp tla2tools.jar tla2tex.TLA -shade -grayLevel 0.90 Spec.tla

TLATeX 对 TLA+ 规范中的对齐很敏感。如果源文件中有：

Action == /\ x'   = x - y
          /\ yy'  = 123
          /\ zzz' = zzz

/\ 和 = 符号会在输出中自动对齐。两位或三位字符宽度的 TLA+ 符号（=>、==、..、++、--、//、**、::、<:、:>）也会被替换为对应的 LaTeX 数学符号命令。

7.6 学习路线

第一步：读完 Lamport 的 TLA+ 视频课程（YouTube 搜索「Leslie Lamport TLA+」），总时长约 5 小时。前 3 课看完就动手写——计数器、互斥锁、生产者-消费者队列，每个只用 20-30 行，不需要复杂的 .cfg。

第二步：找一个工作中接触过的并发或分布式协议——哪怕是一段加了锁的 Go 代码——把它的核心协议抽出来写成 TLA+ 规范。这一步的目标不是找到 bug，是体会"用精确数学公式写清楚一个协议需要哪些信息"。这件事本身就是收获。

第三步：用 TLC 跑模型检验。真正的学习发生在一个循环里：写规范 → TLC 报错 → 阅读 trace → 修正或改进规范 → 重复。

7.7 参考文献

• 《Specifying Systems》, Leslie Lamport. TLA+ 唯一权威文档，涵盖了本文的全部理论基础（包括精炼和公平性的完整形式化处理）。
• 《How Amazon Web Services Uses Formal Methods》, Chris Newcombe et al., 2015. CACM. TLA+ 在工业界实际效果的一手报告。
• Learn TLA+ (learntla.com), Hillel Wayne. 对新手最友好的教程。
• TLA+ 视频课程, Lamport. 黑板授课，没有幻灯片——看 Lamport 在黑板上写 $\Box$ 本身就是一种学习。

尾声

形式化验证并不是银弹。它无法发现需求层面的错误——如果本身对问题理解有偏差，规范写得再精确也是精确地错。它也无法代替集成测试——不能验证性能、不检测内存泄漏、不处理硬件故障。

但它解决了一个其他手段无法解决的问题：对设计本身的逻辑正确性给出数学级别的保证。

在一个分布式系统越来越复杂、并发越来越普遍的年代，这个能力不是锦上添花。单台机器上跑 100 个并发 goroutine，人工推理其安全性就已经不可靠。更何况跨数据中心的一致性协议。

TLA+ 选择了用数学而非代码来描述系统。这个选择在工程界看起来不自然——工程师习惯于可执行的东西。但写规范的目的不是执行，而是推理。数学恰好是人类发明的最强大的推理工具。

你不需要成为形式化验证专家。但如果你在维护任何一个有并发状态的系统，你应该至少能用 TLA+ 把它的核心协议写清楚。光是把「它该怎样工作」翻译为精确的数学公式——这个过程本身就会逼你看到很多被自然语言掩盖的问题。