TLA+ 入门：用 Prompt 驱动形式化验证

通往胜利的提示词：LLM 时代的 TLA+ 入门

大多数工程师对使用 TLA+ 的第一个反对意见是，其语法很不友好。它看起来像 LaTeX，而不像代码。但现在，前沿的 LLM 可以轻松生成 TLA+。你仍然需要负责理解你的系统，定义什么是"正确性"，并且需要对时态逻辑有高层次的理解。本文我将解释时态逻辑。最后我会展示一个示例提示，说明如何使用 Claude 开始编写 TLA+ 规范。

这是一个经典谜题。你有一罐豆子。每个豆子是白色或黑色。罐子开始时不是空的。当至少有 2 个豆子时：

如果它们是同一颜色：丢弃两个，加入 1 个白豆。

如果它们是不同颜色：丢弃两个，加入 1 个黑豆。

豆子的数量能否达到零？

如果算法在 b = 1 时终止，初始状态一定是什么样的？

你可以费力地思考。或者你可以用 TLA+ 写下来，让模型检查器自动回答这两个问题。整个要点就是避免思考——或者至少让机器验证你的思考是否正确。或者让你的朋友相信你的思考是正确的，或者说服你研究论文的同行评审小组。

TLA+ 由 Leslie Lamport 在 1990 年代发明。TLA 代表"Temporal Logic of Actions"（行为的时态逻辑），TLA+ 是这门特定语言的名称。TLA+ 具有基本的布尔逻辑、集合和函数，以及量化（"for all"和"there exists"）。它还具有时态运算符，我们很快就会看到。

当你用 TLA+ 写规范时，你编写的是定义状态机的逻辑公式。该机器有一个固定的变量集，每个状态都是对变量的值的赋值。对于豆罐问题，有变量：w（白豆数量）和 b（黑豆数量）。每个状态都是对 w 和 b 的值的赋值。行为是一个状态序列，规范是一组允许的行为。

我们需要一个初始状态规则——一个谓词，对我们愿意开始的状态恰好为真。用英文说："罐子初始时不是空的"，或 w + b > 0。这些初始状态中哪些与谓词匹配？

b = 0 /\ w = 0
b = 0 /\ w = 4
b = 6 /\ w = 1
b = 1 /\ w = "foo"

在 TLA+ 中，"/" 表示"and"，所以 b = 0 /\ w = 0 表示"b = 0 and w = 0"。

第二和第三个状态与谓词匹配。第一个不匹配，因为 w 和 b 的和为零，最后一个状态没有意义，因为你不能将 1 和字符串"foo"相加。TLA+ 没有类型系统，只有集合，所以没有什么阻止 w 成为字符串。Lamport 称这样的东西为"silly"。我们通过指定 w 和 b 必须是自然数来防止 silly 状态：

EXTENDS Integers
Init == w \in Nat /\ b \in Nat /\ w + b > 0

EXTENDS Integers 导入处理整数所需的所有内容，如自然数集 Nat，\in 是集合成员操作符 ∈。在 TLA+ 中，== 表示"定义为"。这很令人困惑，因为它有点与 C 相反：单个 = 测试相等性，而 == 命名一个公式（如宏）。

状态转移规则是两个状态（当前和下一个）上的谓词，说明哪些转移是合法的。让我们把算法变成 TLA+ 中的状态转移规则。

从英文开始：

2 个白豆：移除 2 个白豆，加入 1 个白豆 → 净效果：w -= 1

2 个黑豆：移除 2 个黑豆，加入 1 个白豆 → 净效果：b -= 2

各 1 个：移除 1 个白豆和 1 个黑豆，加入 1 个黑豆 → 净效果：w -= 1

注意第一和第三种情况对状态的影响相同：都只是从 w 中减去 1，保留 b。这是当你精确地写下来时自然得出的洞察。

在 TLA+ 中，这些变成三个动作：

WW == w > 1 /\ w' = w - 1 /\ UNCHANGED b          \* Picked 2 white
BB == b > 1 /\ b' = b - 2 /\ w' = w + 1           \* Picked 2 black
WB == w > 0 /\ b > 0 /\ w' = w - 1 /\ UNCHANGED b \* Picked 1 of each

这里有两个我们第一次看到的运算符。撇号 (') 运算符表示"这个变量的下一个值"：w' = w - 1 表示"在下一个状态，w 将等于当前的 w 减 1"。UNCHANGED b 是 b' = b 的简写。你必须在每个动作中说明每个变量——TLA+ 不会假设未提及的变量保持不变。这很烦人，但它迫使你思考每个动作对整个状态的影响。

没有撇号的项是保护条件：现在必须满足的条件才能触发动作。带有撇号的项是赋值：下一个状态的样子。如果保护条件为假，动作被禁用。* 开始一条注释（是的，这是反斜杠和星号）。

完整规范如下：

-------------- MODULE beans -----------------
EXTENDS Integers
VARIABLES w, b
vars == <<w, b>> \* convenient list of all variables

Init == w \in Nat /\ b \in Nat /\ w + b > 0

WW == w > 1 /\ w' = w - 1 /\ UNCHANGED b          \* Picked 2 white
BB == b > 1 /\ b' = b - 2 /\ w' = w + 1           \* Picked 2 black
WB == w > 0 /\ b > 0 /\ w' = w - 1 /\ UNCHANGED b \* Picked 1 of each
Next == WW \/ BB \/ WB

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
==============================================

公式 Next 定义为所有三个动作的 OR (/)——在任何给定的状态，任何满足保护条件的动作都是启用的。这是非确定性：规范没有说发生哪个动作，只是说哪些是可能的。模型检查器探索所有这些动作。

Spec 行是任何 TLA+ 规范的脊梁，你会在基本上每个你读到的 TLA+ 规范中看到它。它说："这个规范允许的每个行为都从一个 Init 为真的初始状态开始，每个转移都满足 Next。" WF_vars(Next) 部分的意思是"算法必须不断取得进展——当动作启用时，它不能永远停滞"。这叫做公平性约束，继续关注...

[][Next]_vars 部分隐藏了一些我将跳过的复杂性。如果你想深入理解，请阅读 Lamport 的《Specifying Systems》。出于提示的目的，只需知道它在那里。

状态和行为

行为是一个无限的状态序列，从初始状态开始，其中每一步都由 Next 允许。按约定，行为是无限长的。如果算法终止（到达一个不能进一步执行任何动作的状态），最后状态就永远重复。这种重复叫做 stuttering。所以在 TLA+ 中，"终止"意味着算法到达一个 stuttering 状态并停留在那里。

我们规范中有无限多个初始状态——任何满足 w + b > 0 的自然数对都是有效的初始状态。让我们看一个状态空间的子集，只是以 b=3 和 w=5 开始的状态：

每个节点是一个状态。每条边是一个有效的转移，标记有应用的动作。一些边说"WW/WB"——这是因为当 w > 1 且 b > 0 时，WW 和 WB 都启用并导致相同的下一个状态（都只是将 w 减少 1）。模型检查器探索两个动作但发现相同的后继状态，所以它们合并成一条边。

这个图中的行为是从初始节点到终端节点的路径，然后是 stuttering。这是一个行为：

模型检查器 TLC 从初始状态集开始，应用下一状态关系生成后继状态，并使用哈希（它称之为"fingerprinting"）来避免重新访问已经看过的状态。

当 TLC 发现状态时，它检查不变式和属性。（我们稍后会学习那些是什么，但现在：这些是显示你的规范是否正确的断言。）如果 TLC 发现违反，它报告反例：导致坏状态的一个状态序列。因为它是广度优先搜索，它为不变式违反找到最短的反例（或其中之一）。这对诊断很有帮助——4 步跟踪比 100 步的要容易得多调试。

规范与配置

TLA+ 规范由两个文件组成，beans.tla 包含时态逻辑，beans.cfg 文件包含模型检查配置。为什么是两个文件？规范是系统的理想化描述，其状态空间和行为通常是无限的。你可以用这个规范做很多事情：证明它是正确的，或用它来记录你的算法并向朋友解释，等等。模型检查只是规范的几种用途之一，所以模型检查配置在一个单独的文件中。

当然，如果有无限多个状态，模型检查是不可能的。我们通常必须通过设置初始状态集大小的限制、限制采取的动作数量等来人为地限制状态空间。所有这些限制都应该在配置文件中。

如果你的规范有错误，你通常会在一个小的有界模型中看到它。（我们称之为"small-model hypothesis"。）实际上，第一次检查在第一秒或两秒内捕获明显的错误。如果你运行几个小时而没有发现违反，你会更有信心。界需要有多大才能找到所有错误？那很难说。它必须来自你对算法的推理和直觉。

所以，假设这是 beans.tla（与我上面展示的相同规范）：

-------------- MODULE beans -----------------
EXTENDS Integers
VARIABLES w, b
vars == <<w, b>> \* convenient list of all variables

Init == w \in Nat /\ b \in Nat /\ w + b > 0

WW == w > 1 /\ w' = w - 1 /\ UNCHANGED b          \* Picked 2 white
BB == b > 1 /\ b' = b - 2 /\ w' = w + 1           \* Picked 2 black
WB == w > 0 /\ b > 0 /\ w' = w - 1 /\ UNCHANGED b \* Picked 1 of each
Next == WW \/ BB \/ WB

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
==============================================

这是无界的，无法进行模型检查，因为有无限的初始状态。要限制模型，我可以像这样更新 Init：

CONSTANTS WMAX, BMAX
Init == w \in 0..WMAX /\ b \in 0..BMAX /\ w + b > 0

CONSTANTS
  WMAX = 3
  BMAX = 3

SPECIFICATION Spec

现在有 15 个初始状态，总共 17 个状态。（对你的练习：你能弄清楚为什么是这些数字吗？）

回答问题

我们如何使用模型检查器 TLC 来回答我们的两个问题而不需要太费力地思考？

豆子的数量能否达到零？我们编写一个不变式——一个我们声称在每个可达状态上总是真的状态谓词：

NotEmpty == w + b > 0

我们通过在 beans.tla 中定义它并在 beans.cfg 中引用它来告诉 TLC 检查这个：

INVARIANT NotEmpty

TLC 对整个可达状态图进行广度优先搜索，并确认没有状态违反它。豆罐永远不是空的。

为什么不能？看守卫：每个动作要求至少 2 个豆子才能启用（w > 1、b > 1 或 w > 0 /\ b > 0）。每个动作使豆子总数减少恰好 1。所以一旦你只有 1 个豆子，就没有动作启用，算法终止。你永远不能从 1 变到 0。

如果终止时 b = 1，初始时一定是什么？看 BB，唯一改变 b 的动作。它将 b 减少 2。这意味着 b 的奇偶性（奇数或偶数）从初始状态到结束永远不会改变。所以如果我们以 b = 1（奇数）终止，b 在开始时一定是奇数。我们可以将其表示为一个时态属性——一个公式，覆盖整个行为，而不仅仅是单个状态：

TerminationWithOneBlack == (b % 2 = 1) => <>[](b = 1 /\ w = 0)

阅读这个为："如果 b 是奇数，那么最终 b 将是 1，w 将是 0。"

这使用两个时态运算符：<>（diamond，表示"eventually"）和 []（box，表示"always"）。结合为 <>[],，它们表示"最终达到一个状态并停留在那里"——这正是终止。

我们在 beans.tla 中添加定义并在 beans.cfg 中引用它：

PROPERTY TerminationWithOneBlack

我在 beans.cfg 中使用 PROPERTY，因为这是一个时态属性（它使用时态运算符并应用于整个行为），而不是像我为 NotEmpty 所做的 INVARIANT。TLC 验证这个属性在所有行为中都成立，确认从奇数 b 开始的任何行为都以 b = 1 终止。

但等等——如果 b 是奇数，最终 b=1 和 w=0 真的成立吗？如果 b 是奇数而状态机只是坐在那里什么都不做怎么办？这就是公平性约束 WF_vars(Next) 确保的。它说如果 Next 持续启用（即其中一个动作被启用，因为有至少两个豆子），那么它最终会执行。这对于任何"eventually"属性为真是必要的。

时态运算符

时态逻辑在普通一阶逻辑之上添加了两个核心运算符，你可以以有趣的方式组合它们。

<>P（最终 P）：在这个行为的某个时刻，P 是真的。如果 P 短暂闪现然后停止，那仍然算数。

[]P（总是 P）：在这个行为的每个时刻，P 都是真的。这基本上就是不变式所说的，只是表示为时态公式。

<>[]P（最终总是）：P 最终变为真并永远保持真。这是表示稳定终止的方式：系统达到一个好状态并永远不会离开。

[]<>P（总是最终）：P 不断地无限次返回。P 为假可能有很长的间隙，但它总是回来。这是表达"锁总是最终可获得的"或"队列总是最终被清空"这样的东西的方式。

注意，<>[]P 严格强于 []<>P。如果 P 最终稳定为永远真，它肯定会不断返回。但 P 可以不断返回而永远不稳定。

我提示 Claude 为豆罐问题编写一个规范：

> write me a TLA+ spec for the following toy example.

there's a can of w white and b black beans, at least one bean initially.

at each step, if there are at least 2 beans, remove 2. if they're the same color, discard both and add 1 to w, if they're different, discard both and add 1 to b.

use the spec to reason: can the number of beans reach 0? what initial state is necessary to terminate with b=1? 

download TLC 1.8.0 and run the model-checker to find the answers.

我告诉它下载 TLC 1.8.0，这是当前的预发布版本，因为上一次官方 TLC 发布是几年前。不出所料，Claude 一次性编写了一个通过模型检查并回答问题的规范。但这是一个非常简单的任务。

LLM 基本上消除了 TLA+ 的第一个进入门槛：其语法。定义系统必须维护什么属性仍然是你的工作；Hillel Wayne 发现它们在编写这些方面做得不好。弄清楚你现有系统实际如何表现也是你的工作。即使有强烈的引导，LLM 也不能读取现有系统的代码并将其转换为 TLA+ 规范。所以你还没有完全摆脱思考。但 LLM 已将 TLA+ 从一个不透明的思考工具转变为一个半透明的工具。