跳转至

TLA+ 到底能验证什么，又无法验证什么？从并发系统设计到 AI 编码的形式化边界

What TLA+ Can and Can't Check

文章背景与核心概要

近期，Claude Code 创造者 Boris Cherny 透露 Opus 成功运用形式化规范语言 TLA+ 发现了代码中的并发竞态条件，引发了技术社区对形式化验证与 AI 智能体编程结合的热烈探讨。著名 TLA+ 布道者与教育家 Hillel Wayne 撰文指出，尽管 TLA+ 在设计复杂并发系统、杜绝逻辑缺陷方面威力惊人，但它绝非能够一劳永逸解决 AI 软件开发难题的“银弹”。本文系统梳理了 TLA+ 原生支持验证的状态不变量与时序活性属性，深入剖析了它无法原生表达多步动作、可达性及超属性等关键盲区，并探讨了工程师采用的精巧变通方案与其局限。这一辨析清晰划定了形式化方法与自动化编码的能力边界，为理性看待 AI 辅助工程系统设计提供了极为清醒深刻的技术视角。

核心概述

Summary

最近，随着利用 AI 智能体 (AI Agent，例如 Claude Code 和 Opus) 借助 TLA+ 排查竞态条件 (Race Condition) 的演示引爆技术圈，形式化验证 (Formal Verification) 再次掀起了全网热议。诚然，TLA+ 是设计复杂并发系统 (Concurrent Systems) 、验证系统安全性 (Safety) 与活性 (Liveness) 属性时近乎无往不利的神兵利器，但它绝非万能的“银弹”。本文将深入探讨 TLA+ 原生能够表达与检验的逻辑边界、它无法直接表达的关键盲区 (例如可达性、超属性以及跨多步动作) ，并揭示工程师为了拓展其能力上限所采用的各种精妙 (却略显繁杂) 的变通技巧。

Following recent excitement around using AI agents (like Claude Code and Opus) to find race conditions via TLA+, formal verification has sparked widespread internet discussion. While TLA+ is an exceptionally powerful tool for designing complex concurrent systems and verifying safety and liveness properties, it is not a silver bullet. This article explores what TLA+ can express and check natively, the notable limitations regarding what it cannot express (such as reachability, hyperproperties, and multi-step actions), and the clever (yet messy) workarounds engineers use to stretch its capabilities.

引言

Introduction

上周，Claude Code 的创造者 Boris Cherny 透露，Opus 能够借助 TLA+ [^tla] 成功定位代码中的竞态条件。

Last week Boris Cherny, the inventor of Claude Code, mentioned that Opus was able to use TLA+[^tla] to find race conditions in code.

一时间，整个互联网都在热烈探讨形式化验证。

And now everybody on the internet is talking about formal verification.

作为一名长年深耕 TLA+ 教学 ( 1 2 ) 与积极 倡导者 的同行者，看到这种现象我确实感到振奋！TLA+ 在设计复杂并发系统并确保其免受逻辑 Bug 困扰方面表现极其出色。 [^antithesis] 但与此同时，作为一名始终主张理性思考的技术人，这种近乎盲目的狂热又令我深感担忧。我看到许多人断言：形式化方法 (Formal Methods) 将一劳永逸地彻底解决智能体驱动软件开发中的可靠性问题——而这完全是无稽之谈。

As a long-time educator (1 2) and advocate of TLA+, this is really exciting! TLA+ is great at designing complex concurrent systems and making sure they're bug-free.[^antithesis] 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.

关于 TLA+ 在实际保证能力上的局限性，业界已经有过汗牛充栋的讨论，例如 正确的设计并不会自动转化为正确的代码实现 。因此，在本次通讯中我想探讨一个截然不同的局限维度：要验证一个属性，前提是你必须能够把它描述出来！那么，到底有哪些属性是 TLA+ 根本连表达都无法表达的？

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+ 的基础知识。如果你完全是初学者，建议先阅读上文提到的 [1] [2] 两处资料，或者 阅读这篇入门文章 。)

(This assumes some basic knowledge of TLA+. If you're a total beginner, check out those [1] [2] things above or read here.)

TLA+ 能够验证什么

What TLA+ Can Check

TLA+ 将整个系统的运行过程划分为一组行为 (Behavior) 。每个行为都是一条状态序列，好比“一号红绿灯是绿灯，接着变黄灯，最后变红灯”。在每个状态中，我们可以用常规的布尔表达式来描述现状，比如“四号灯为绿灯”或“所有灯都是红灯”。此外，我们还可以借助三个“时序”逻辑运算符来扩展表达式的表达能力：

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:

  • []P (即“始终为 P”) ：如果 P 在当前状态以及后续每一个未来状态中均成立，则该式为真。例如：[](at_most_one_green) 表示从当前开始的每一个状态中，绿灯的数量绝不会超过一盏。
  • P' (即“P 的后继状态 / P prime”) ：如果 P 在紧邻的下一个状态中为真，则该式为真。例如：light="green" && light'="red" 表示信号灯从绿灯变为红灯。
  • <>P (即“最终为 P / eventually P”) ：如果 P 在当前状态或未来至少某一个状态中为真，则该式为真。例如：<>(light4 = "yellow") 表示四号灯当前是黄灯，或者在未来的某个状态中必定会变为黄灯。
  • []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 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 ("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 在每个初始状态中都成立；而根据“始终” (Always) 的逻辑定义，这意味着从该初始状态出发的每一个未来状态中 P 均成立，即 P 在所有行为的每一个状态中都为真。我们将此称为不变量 (Invariant) ，它是我们在 TLA+ 中验证的最核心、最基础的属性之一。

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+.

我们还可以将 [] 与带撇的后继状态标记 ' 结合，构建出动作属性 (Action Properties) ，或者说状态跃迁的变式。例如 [](x' >= x) 表示 x 的新值始终大于或等于其旧值。另一个有趣的例子是 [](P => P')：一旦 P 为真，它就永远不可能再次变为假。实际的 TLA+ 规范由于引入了一种名为“停滞不变性” (Stutter-Invariance) 的机制而略微复杂一些，不过那属于更深层的实现细节。动作属性与不变量同属于安全性 (Safety) 属性，用通俗的语言来说就是“坏事永远不会发生”。 我曾专门写过一篇文章探讨安全性与活性 。

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. The actual TLA+ is a little more complicated because of a thing called "stutter-invariance", but that's extra details. Action properties and invariants are both safety properties, which roughly means "something bad never happens". I wrote an article on safety and liveness here.

顺便提一下，活性 (Liveness) 指的是“好事最终总会发生”。所有的活性属性都是基于 <> 构建的。单纯的 <>P 仅表示“在每条行为中，P 至少在某一个状态下成立”，对于系统规范而言，这种约束通常太弱了。但通过逻辑复合，我们可以构建出更丰富、更有价值的活性属性：

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:

  • []<>P ：如果从任意状态出发，P 在未来的至少一个状态中必定为真，则该式为真。这通常用来建模故障恢复机制，比如“只要节点发起新的主节点选举，它们最终总能达成共识选出主节点”。
  • <>[]P ：如果在某个时间点之后，P 变为真且此后永远保持为真，则该式为真。这非常适合用来证明算法能够正确终止并收敛到正确结果。
  • [](P => <>Q) ：如果在 P 成立的每一个状态之后，总存在一个使 Q 成立的未来状态，则该式为真。这可以证明因果关系，比如证明 P 最终必定触发 Q，或者“投递到队列中的所有消息最终都会出现在读者的读取历史中”。由于该公式的逻辑书写较为冗长，TLA+ 提供了语法糖 P ~> Q (即 P leads to Q，P 最终导致 Q) 。
  • []<>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 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 => <>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, or that "all messages put on the queue are eventually in a reader's history." Parsing the formula is a little confusing, so we have the sugar P ~> Q (P leads to Q).

虽然 TLA+ 还提供了像 ENABLED 和 <<A>>_v 这样能玩出更多花样的运算符，但我们在实际工程中检验的大多数属性依然是不变量、动作属性与活性属性。此外还有 精炼 (Refinement) ，精炼是安全性和活性的综合体，本身就是一个值得专门立题深聊的庞大概念。

There's a couple of other operators, like ENABLED and <<A>>_v, which open up other tricks, but the majority of the stuff we check are invariants, action properties, and liveness. And refinement, which is a combination of safety and liveness and a topic unto itself.

TLA+ 无法做到的事

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. And, unfortunately, a lot of important properties we care about fall into this category.

其次是一些过于具体的细节限制。TLA+ 的安全性属性要么作用于单个独立状态 (如不变量) ，要么作用于单步跃迁 (如动作属性) 。你无法原生定义一个跨越两步或更多步骤的属性，比如“按下 delete 键紧接着按下 undo 撤销键，系统将完全恢复到初始状态”，或者“按下 power 电源键后，计算机必须在十步之内成功开机”。此外，我们既无法直接对浮点数运算定义属性，也无法对 物理真实时间进行定义，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+ 的属性在语义上默认隐含了针对“所有行为”的全称量词量化。我刚才提到检查 []P 意味着“P 在每一个状态下都为真”，但其实质含义是：“对于系统可能产生的所有行为，[]P 在该行为的初始状态上均成立”。换言之，TLA+ 能够检验的任何系统属性，都必须在每一个单独的行为路径上各自成立。

Now for 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!

其一，我们无法表达“存在至少一条行为使得 P 为真”。也就是说，我们无法直接断言某种状态 P 是可能发生的，哪怕我们在某次执行中并未真正触发它。一个典型的例子是证明“一款游戏是存在通关可能的”。我们把这类属性称为 可达性属性 (Reachability Properties) 。更高级的可达性属性还包括“从任意初始状态出发 P 都是可达的”，或者“从任何满足 Q 的状态出发 P 都是可达的”。

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. More advanced reachability properties would be things like "P is reachable from every initial state" or "P is reachable from any state where Q is true".

其二，我们无法跨越一组行为集合来定义属性。在形式化理论中，这被称为超属性 (Hyperproperty) 。假设我们正在对手机硬件进行建模，希望验证“省电模式消耗的能量始终低于普通模式”。这一属性表述为：“在执行任意相同的动作序列时，省电模式下的功耗绝不高于普通模式”。如果要推翻这个结论，你必须同时给出两条行为路径进行对照：这两条路径除了一个始于省电模式、另一个始于普通模式外完全一致，且普通模式的功耗更低。仅凭单一的行为轨迹根本无法完成这种跨轨迹对比，因此这在 TLA+ 中是无法自然原生检验的。

We also can't define properties over a set of behaviors. This is called a hyperproperty. Say we we're modeling phone hardware and want to verify that energy saving mode always uses less energy than normal mode. The property is "any sequence of actions uses no more power in energy saving mode than in regular mode." To refute this, you'd need to give me two behaviors that were identical except one starts in energy saving mode and the other does not, and the regular mode uses less power. One single behavior isn't enough to cut it, so this is impossible to naturally check in TLA+.

超属性听起来可能有些小众，但它实际上涵盖了 海量的安全属性 (例如信息流的非干涉性) 以及所有统计学意义上的属性 (比如“95% 的响应时间必须在 5 毫秒以内”) 。

Hyperproperties might seem niche but they cover a ton of security properties and all statistical properties ("the 95%ile response time is 5ms").

最后一点稍偏学术化：我们无法将属性定义在全局的状态空间 (State Space) 之上。例如，我们无法断言“从状态 X 到状态 Y 之间存在且仅存在一条路径”。我不太确定这种约束在工程实践中具体有多大用处。大多数这类“元属性” (Metaproperties) 似乎都有潜在的理论价值，但我目前还无法举出十分具体的现实应用场景。

Finally, and this one's a little more academic, we can't define properties over the state space as a whole. We can't say, for example, that there's only one path from state X to Y. I don't know how useful this would be in practice. Most of these kinds of "metaproperties" seem like they have potential to be meaningful, I just don't know what specifically.

所谓的 TLA+ “能够”做到的那些事

What "TLA+" "Can" "Do"

说 TLA+ 做不到这些事情，其实我在一定程度上做了简化。更准确的表述是：如果你编写的形式化规范直接与你打算构建的系统严丝合缝地一一对应，那么 TLA+ 确实无法将这些需求原生表达为系统的固有属性。但是，你可以通过 辅助变量 (Auxiliary Variables) 来 模拟 两步跃迁属性，比如将所有状态变更都记录在一个 state_history 序列中，然后针对该序列定义不变量。你也可以借助 自组合 (Self-Composition) 来模拟部分超属性——在自组合规范中，每一次行为实际上并列模拟了真实系统中的两条执行轨迹。此外，TLA+ 的核心模型检测器 (TLC) 能够通过新引入的 REACHABLE 关键字 检查最基础的可达性属性，并通过 TLCGet 检查某些状态空间属性。Andrew Helwer 甚至写过一篇 堪称硬核疯狂的博文，介绍如何利用公平性与“机器闭包”来模拟“始终可达” 。

I kind of oversimplified when I said that TLA+ can't do these things. I mean that if you are writing a spec, and that spec directly corresponds to the system you want to build, then TLA+ can't express these as properties of your system. But you can mimic two-step properties with auxiliary variables, like storing all state changes in a state_history sequence and defining the property as an invariant on that sequence. You can mimic some hyperproperties with self-composition, where each behavior of the self-composed spec is two behaviors of the actual system. The main TLA+ model checker (TLC) can check the most basic reachability properties with the new REACHABLE keyword and some state-space properties with TLCGet. Andrew Helwer has a crazy post about mimicking "always reachable" with fairness and "machine closure."

这些变通技巧确实行之有效，但归根结底它们依然是“打补丁”式的 Hack。构想出每一个巧妙方案都需要极高的智力成本，并且伴随着严重的副作用：辅助变量会彻底破坏规范的精炼映射；自组合会导致状态空间呈指数级爆炸式膨胀，等等。这些奇技淫巧无法与 TLA+ 的其他高级特性良好组合，也无法覆盖实际需要表达的各种幽微细节。而最糟糕的是，它们会让你的规范模型变得极其怪异且凌乱，严重脱离你真实要实现的软件系统。

These are useful hacks, but they're still hacks. Each one takes a lot of cleverness to figure out and comes with serious drawbacks. Auxiliary variables ruin refinements, self-composition exponentiates your state space, etc. Hacks don't compose well with the other TLA+ features and don't cover all the intricacies of properties you'd want to express. And worst of all, they make your models look weird and messy and not correspond to your actual systems.

当然，你也可以选择专注于其他维度的工具：例如计算树逻辑 (CTL) 可以轻松验证可达性属性；PRISM 专长于概率统计属性的检验，等等。但这种权衡的代价是，它们在 TLA+ 所擅长的领域往往表现逊色，而且对于那些人类无法用逻辑公式清晰表达的现实属性，任何工具同样束手无策。

You could also use a different tool with a different focus. CTL can do reachability properties, PRISM probabilistic properties, etc. They trade off by being worse at things that TLA+ can do, and of course none of them handle properties we can't express logically.

归根结底，TLA+ 非常擅长摘取系统设计中那些“唾手可得的低垂果实”——不变量与活性已经足以覆盖我们日常关心的绝大部分核心问题，而 TLA+ 在表达和验证这两类属性上确实表现不俗。在借助 TLA+ 检验大模型凭借直觉写出的“感觉流代码” (Vibe Coding) 方面，蕴藏着巨大的应用潜力 (同时也伴随着 大量的深坑陷阱 ) 。但我们必须清醒地认识到：现实中仍有许多属性是它根本连表达都表达不了的，更遑论去自动化检验了。

Ultimately TLA+ is pretty good at picking a lot of low hanging fruit—invariants and liveness cover many things we care about, and TLA+ is reasonably good at expressing and checking them. There's a lot of potential (and a lot of pitfalls) in using TLA+ to check vibe code. But there are also many things it cannot even express, let alone check.

《面向程序员的逻辑学》线上演讲回放

Logic for Programmers Talk Online

感谢所有参加上周直播的朋友！你可以在 这里 观看完整的演讲录像。

Thanks to everybody who came to last week's livestream! You can watch the whole thing here.

尾注

Footnotes

  1. “动作时序逻辑” (Temporal Logic of Actions) 。这是一种专为发现并发系统中的 Bug 而设计的形式化规范语言。 这里有关于该名称由来的详细解释 。 ↩
  2. (至于为什么一个对形式化方法如此狂热的人会 加入一家软件测试公司 ，好吧，他们官方博客很快就会有一篇专门的文章来解释这件事。) ↩
  1. "Temporal logic of actions". It's a specification language used to find bugs in concurrent systems. Here's an explanation of the name. ↩
  2. (And as for the question of why a person so evangelical about formal methods joined a testing company, well, there should be an article on their blog about that soon.) ↩