What TLA+ can and can’t check

TLA+ 能检查什么，不能检查什么

September 30, 2026 2026年9月30日

Let’s chill just a little bit on the “TLA+ will save AI from itself” narrative. Last week Boris Cherny, the inventor of Claude Code, mentioned that Opus was able to use TLA+ to find race conditions in code. And now everybody on the internet is talking about formal verification. As a long-time educator and advocate of TLA+, this is really exciting! TLA+ is great at designing complex concurrent systems and making sure they’re bug-free. As a long-time advocate of level-headedness, this new euphoria worries me. I read a lot of people saying that formal methods will solve the problem of agentic software development once and for all, and that’s nonsense. Enough words have been spilled about the weaknesses of TLA+ in terms of what it can guarantee, like how correct designs don’t automatically translate into correct code. So I’d like to focus on a different limitation for this newsletter: to verify a property, we need to have a property to verify! So what are the properties that TLA+ can’t even express? 让我们稍微冷静一下“TLA+ 将拯救 AI 于水火”的叙事。上周，Claude Code 的发明者 Boris Cherny 提到 Opus 能够使用 TLA+ 来发现代码中的竞态条件。现在互联网上的每个人都在谈论形式化验证。作为一名长期的 TLA+ 教育者和倡导者，这确实令人兴奋！TLA+ 在设计复杂的并发系统并确保其无 bug 方面非常出色。但作为一名长期的冷静倡导者，这种新的狂热让我感到担忧。我读到很多人说形式化方法将一劳永逸地解决智能体软件开发的问题，这简直是胡说八道。关于 TLA+ 在保证能力方面的弱点，已经有太多的讨论了，比如正确的架构设计并不能自动转化为正确的代码。因此，我想在本期通讯中关注另一个局限性：要验证一个属性，我们首先得有一个可以验证的属性！那么，有哪些属性是 TLA+ 甚至无法表达的呢？

What TLA+ can check

TLA+ 能检查什么

TLA+ divides the system into a set of behaviors. Each behavior is a sequence of states, like “light one is green, then yellow, then red”. In each state we can express a regular boolean expressions like “Light four is green” or “All lights are red.” We can also modify expressions with three “temporal” logical operators: TLA+ 将系统划分为一系列行为。每个行为都是状态的序列，例如“一号灯是绿色，然后是黄色，最后是红色”。在每个状态中，我们可以表达常规的布尔表达式，如“四号灯是绿色”或“所有灯都是红色”。我们还可以使用三个“时序”逻辑运算符来修饰这些表达式：

• []P (“always P”) is true if P is true in the current state and every future state. Example: [](at_most_one_green) is true if every state going forward has no more than one green light. []P（“总是 P”）：如果 P 在当前状态及所有未来状态中均为真，则该表达式为真。例如：[](at_most_one_green) 表示在未来的每一个状态中，绿灯的数量不超过一个。
• P’ (“P prime”) is true if P is true in the next state. Example: light="green" && light'="red" is true if the light changes from green to red. P’（“P 的下一状态”）：如果 P 在下一个状态为真，则该表达式为真。例如：light="green" && light'="red" 表示灯从绿色变为红色。
• <>P (“eventually P”) is true if P is true in the current state or in at least one future state. Example: <>(light4 = "yellow") is true if light4 is yellow or is yellow in a future state. <>P（“最终 P”）：如果 P 在当前状态或至少一个未来状态中为真，则该表达式为真。例如：<>(light4 = "yellow") 表示四号灯现在是黄色，或者在未来某个状态会变成黄色。

When we say that P is a property of the system, we mean it is true in the initial state of every behavior. So if we check the property []P, that means that []P is true in every initial state, and then by the definition of “always” means that P is true in every future state from that initial state, meaning it is true in every state of every behavior. We call this an invariant, and is one of the most foundational properties we check in TLA+. 当我们说 P 是系统的一个属性时，是指它在每个行为的初始状态下都为真。因此，如果我们检查属性 []P，意味着 []P 在每个初始状态下都为真，根据“总是”的定义，这意味着 P 在从该初始状态开始的每一个未来状态中都为真，即它在每个行为的每一个状态中都为真。我们称之为“不变性”（invariant），这是我们在 TLA+ 中检查的最基础的属性之一。

We can also compose [] with primes to get action properties, or change variants. [](x' >= x) is true if the new value of x is always greater than equal to the old value of x. Another fun one is [](P => P'): once P is true, it can never become false again. 我们还可以将 [] 与撇号（primes）组合来获得动作属性或变化变体。[](x' >= x) 表示 x 的新值总是大于或等于旧值。另一个有趣的例子是 [](P => P')：一旦 P 为真，它就永远不会再变为假。

Action properties and invariants are both safety properties, which roughly means “something bad never happens”. Liveness, btw, is “something good always happens”. All liveness properties are based off of <>. By itself, <>P just means “P is true in at least one state of every behavior”, which is usually too weak to be a good system property. But with composition, we can make more interesting liveness properties: 动作属性和不变性都属于安全性属性，大致意味着“坏事永远不会发生”。顺便提一下，活性（Liveness）意味着“好事总会发生”。所有的活性属性都基于 <>。单独使用时，<>P 仅表示“P 在每个行为的至少一个状态中为真”，这通常太弱，不足以成为一个好的系统属性。但通过组合，我们可以构建更有趣的活性属性：

• []<>P is true if, in every state, P is true in at least one future state. This can represent recovery mechanisms like “If the nodes have a new leader election, they will eventually agree on a leader.” []<>P：如果在每个状态下，P 在至少一个未来状态中为真，则该表达式为真。这可以表示恢复机制，例如“如果节点进行了新的领导者选举，它们最终会就领导者达成一致。”
• <>[]P is true if, at some point in time, P becomes true and remains true forever. This is great for showing that algorithms terminate with the correct results. <>[]P：如果在某个时间点，P 变为真并永远保持为真，则该表达式为真。这非常适合证明算法以正确的结果终止。
• [](P => <>Q) is true if, for every state where P is true, there is a future state where Q is true. This can do things like show that P eventually causes Q. [](P => <>Q)：如果对于 P 为真的每一个状态，都存在一个 Q 为真的未来状态，则该表达式为真。这可以用来证明 P 最终会导致 Q。

What TLA+ can’t do

TLA+ 不能做什么

Let’s start with the obvious one: if you don’t know how to represent your property as a logical formula, then TLA+ can’t help you. Nor can any formal method. If you can’t formalize the human notion of a bird, you can’t prove your app recognizes birds. 让我们从最显而易见的一点开始：如果你不知道如何将你的属性表示为逻辑公式，那么 TLA+ 就帮不了你。任何形式化方法也都帮不了你。如果你无法将人类对“鸟”的概念形式化，你就无法证明你的应用程序能识别鸟。

Next, the overly specific things. TLA+ safety properties work on the level of either individual states (invariants) or single step (action properties). You can’t natively define a property over two or more steps, like “pressing delete and then undo gives you back the original state”, or “once power is pressed, the computer turns on within ten steps”. We also can’t define properties on floating point operations or over real time, just logical time. 接下来是过于具体的问题。TLA+ 的安全性属性工作在单个状态（不变性）或单步（动作属性）的层面上。你无法原生定义跨越两步或多步的属性，例如“按下删除键然后撤销会恢复到原始状态”，或者“按下电源键后，计算机在十步之内启动”。我们也不能在浮点运算或实时时间上定义属性，只能在逻辑时间上定义。

Now for the limit that most interests me. TLA+ properties are implicitly quantified over all behaviors. I said that checking []P means “P is true in every state,” but what it actually means is “for all behaviors, []P is true of that behavior’s initial state.” Any property TLA+ can check of the system must be a property that is true for every individual behavior. What does that leave out? A lot more than you’d expect! For one, we can’t do “there exists a behavior where P is true”. So we can’t say that P is possible, even if we don’t actually reach it. One example of this would be proving that a game is winnable. We call these reachability properties. We also can’t define properties over a set of behaviors. This is called a hyperproperty. 现在谈谈我最感兴趣的局限性。TLA+ 属性隐式地量化了所有行为。我说检查 []P 意味着“P 在每个状态下都为真”，但它实际的意思是“对于所有行为，[]P 在该行为的初始状态下为真”。TLA+ 能检查的任何系统属性，都必须是对于每一个独立行为都为真的属性。这遗漏了什么？比你预想的要多得多！首先，我们无法表达“存在一个行为使得 P 为真”。因此，我们无法断言 P 是可能的，即使我们实际上并没有达到它。一个例子是证明游戏是可赢的。我们称这些为可达性属性。我们也不能定义跨越一组行为的属性。这被称为超属性（hyperproperty）。