本周鲍里斯·切尔尼（Boris Cherny）发推文推介了有30多年历史的形式化建模工具包动作时序逻辑加（TLA+）。他用奥普斯5.5（Opus 5.5）在TLA+和精益（Lean）中建模了克劳德代理软件开发工具包（Claude Agent SDK）的部分内容，互联网反响热烈：约100万浏览量、数千书签，人们询问TLA+究竟是什么。他的帖子是极佳展示，并补充了达多格（Datadog）关于harness-first agents的早期例子。

鲍里斯发推，网友竞相转发

本周鲍里斯·切尔尼发了一条推文，让已有 30 多年历史的形式化建模工具 TLA+ 受到关注。他用 Opus 5.5 在 TLA+ 和 Lean 中建模了 Claude Agent SDK 的部分内容，互联网随即给出惯常反应：近百万浏览、数千收藏，大家都在问 TLA+ 到底是什么。鲍里斯的帖子是很好的展示，也补充了早期案例，说明在智能体编程中投入精力学 TLA+ 非常值得，比如 Datadog 关于 harness-first agents 的帖子。

如果你也正好奇 TLA+ 是什么、有什么用，那就找对地方了。TLA+ 是我们团队深入研究的形式化技术之一。我们关注它还有更广的原因：TLA+ 提供了一种紧凑的语言，用来描述系统允许做什么、以及什么必须始终或最终为真。这是验证的好起点，但故事不止于此。

简短版如下：

• TLA+ 描述可能的系统行为，以及这些行为应满足的性质。
• TLA+ 本身并不能完全验证实现。 它检查的是软件的模型而非软件本身，且其主模型检查器只探索有限实例。
• 现代证明系统能带我们走得更远。 在 Verus 中，规范、证明和 Rust 实现可以存在于同一种语言里。
• AI 已经能自动化部分流程。 我们搭建了一个智能体流水线，将 16000 多对 TLA+ 规范/性质对转化成了 3000 多个机器检查的 Verus 证明。

那么，有趣的问题不止是智能体能否写出 TLA+

而是当智能体能在规范、证明和真实程序间移动时，什么会变得可能。我们在 Reasonable 的部分工作，就是训练模型让智能体能稳定、可靠、快速地做到这一点。

什么是 TLA+

我们的贯穿例子是下方交互 playground 里的场景：三台计算机 a、b、c 必须就谁是领导者达成一致。数据库依赖领导者选举的正确性。我们要求不能同时存在两个领导者。你可以通过这个 playground 的五关游戏学习 TLA+ 基础。

TLA+（时序动作逻辑）是一种用来写下两类对象的语言：

• 转移系统：系统能做什么。 包含状态（系统的快照，如谁是候选、谁投了谁、谁是领导）和动作（改变状态的单步，如“a 发起选举”、“b 投给 a”）。在交互 playground 中，你手动执行这些步骤，像测试者那样探索一种可能的运行。
• 时序性质： 关于运行如何随时间展开的陈述。例如“从未有两个领导者”、“最终会选出领导者”。

TLA+ 模型声明合法的系统状态以及这些状态间允许的转移。例如选举中，a、b、c 任一都可从初始状态发起选举并投给自己，b 可以投给 a 或 c。它对转移不规定顺序，也不试图建模不同事件发生的概率分布，这对分布式系统正合适，因为消息、超时和用户操作可能以多种顺序发生。

其底层数学很简单，用集合、真假陈述和关系。时序性质由执行上的算子构建：

• □ P（总是 P）：P 在每个访问到的状态都成立。
• ◇ P（最终 P）：P 在某个未来状态成立。
• P ⇝ Q（P 导致 Q）：每当 P 成立，之后 Q 最终成立。

有两类性质尤其常被关注。

安全性：坏事永不发生。我们的选举：□（从不出现两个领导者）。playground 中模型检查器探索每个可能状态：三台机共 38 个状态，确认该性质。第 2 关改了一条规则让计算机可投两次，检查器返回一个六步执行以两个领导者告终。该执行是反例：模型违背性质的具体方式。

活性：好事终将发生。只有安全不够，永远不动的系统绝对安全。所以我们还要求：◇（某人是领导者）。第 3 关显示为何重要：一个笔误让什么都没发生，安全检查仍通过。活性需要公平性假设，排除某动作永远可能却从不执行的情况。弱公平 WF(A) 说持续启用的动作必须最终发生；强公平 SF(A) 覆盖无限次启用的动作。

心智模型很简单：TLA+ 模型描述系统可能的执行轨迹，性质描述哪些轨迹可接受。验证问的是否每条可能轨迹都可接受。TLC 标准模型检查器通过枚举有限实例的可达状态回答。证明则更强地声明性质普遍成立。

TLA+ 不是什么

TLA+ 因这种推理方式实用而部署渐广，可在 AWS、MongoDB、Datadog、Kafka 等见到。但有三个重要告诫，TLA+ 单独不足以完成全套软件验证。

模型检查只走这么远。实践中常用 TLC，它探索每个可能运行但仅限有限模型。例子中状态空间从三台机 38 态涨到九台机超百万态。要确立任意系统规模的性质需证明。TLA+ 自带证明器 TLAPS 某些情况可行，但自动化有限，尤其活性论证。

模型不是实现。TLA+ 规范通常是软件的独立模型。无自动保证实现完全像模型，代码改动时两者可能偏离。这是经典规范-实现鸿沟的一环。

TLA+ 不能表达每个想要的性质。TLA+ 基于线性时序逻辑，对单个执行陈述：“每轮最终选领导者”。但有些性质关乎替代未来或策略。

• CTL 分支时间逻辑，可表达：“任意状态仍能发起新选举。”
• ATL 可表达策略陈述：“无论他人如何，此计算机有策略成为领导者。”

这些更富性质在思考含多竞争或协作智能体系统时相关。所以 TLA+ 给了描述时序行为的极有用语言，但完整验证栈需更多：更强证明机制、与真实代码连接、更富逻辑。

从 TLA+ 到证明

一条路径是把模型带入现代证明系统。有几种选择，例如：

• Lean 交互式：你（或 AI）逐步写证明。很通用，数学常用，也是鲍里斯帖所用证明器。
• Verus 自动活跃型，围绕 Rust 设计。你提供规范和重要证明结构，自动求解器处理大量底层推理。
• Veil 基于 Lean 专为国家机模型造的工具。Leo de Moura 推荐，近期用于验证同步引擎并修了 17 个 bug。但活性仍是未来工作，验证模型仍独立于实现。

为何用 Verus？因为规范和证明可与真实 Rust 实现共处。这重要，因它提供缩小规范-实现鸿沟的路径：不只证明独立抽象模型的性质，最终可证实现精化该模型。如 Anvil 已展示此验证风格；我们在 Reasonable 的工作尤其基于 Anvil。

为何自动化形式验证？涉及的证明常不如“形式验证”一词听起来那么异类。

• 安全证明通常归纳式。 证性质初始成立，再证每动作保持它。大量工作是按不同动作拆分并跟踪相关不变量。
• 活性证明确立进展。 通常某量随系统推进递减，加公平性假设排除启用动作被无限推迟的执行。WF1、WF2、SF1、SF2 等规则封装这些论证；我们的时序库将它们实现为已证 Verus 引理。

大量此工作重复：跟踪不变量、按动作拆分、提供中间引理、填求解器可见细节。这使其成为证明生成智能体的天然目标。

从证明到机器可检查软件

自动定理证明近期数学进展快。软件验证问题稍异：证之前需对软件意图的有用描述。TLA+ 在此吸引人，因时序规范紧凑可读，且许多真实系统已有 TLA+ 模型。若能连这些模型到现代证明系统和实现，多方向可行。

• 精化证明。 证 Rust 实现遵循 TLA+ 模型。Anvil 手动展示。更多自动化可缩小验证模型与验证实现间的鸿沟。
• 程序综合。 从模型出发生成实现及证明其精化的证明。此设定中形式规范同时约束代码生成与验证。
• 协议搜索。 一旦检查候选协议足够廉价，验证器可成目标函数：生成协议变体、验证、保留满足性质者。这开始像 AlphaEvolve，但正确性由形式而非测试估计。
• 超越线性时间。 多智能体系统某些性质关乎替代未来或策略而非单执行轨迹。表达需超 LTL 逻辑。Benjamin Brast-McKie 工作探索此面，我们当前工作聚焦证时序性质并连到程序。

我们的进展抢先看

我们一直在做将 TLA+ 规范译为机器可检 Verus 证明的流水线。后续博文详述各块。目前主要结果：

• TLA+ 到 Verus 转译器。 建了算法转译器，并与智能体替代方案（LLM 翻译、另一 LLM 审查）比较。
• 带防作弊的检查器-审查器循环。 一智能体写证明另一审查。独立把关者检查智能体是否改规范或引入如 assume(false) 的捷径。
• Verus 时序证明数据集。 从 16459 对真实 TLA+ 规范/性质对，流水线产出超 3000 个机器检查的安全与活性证明。还建了 40 任务评估集。
• 当前模型评估。 测了闭源和开源前沿模型在评估集上的表现，看其能完成哪些时序证明及剩余失败模式。

讨论整体对 TLA+ 本身评价不低，但对这篇文章的表达方式以及「用 AI 把形式化验证封装起来」的叙事分歧很大：一派认为 AI 已经能靠不变量抓到真实并发缺陷，另一派担心模型与实现同步、验证可信度，以及把推理过程对人隐藏。

认为文章写作糟糕，削弱了 TLA+ 的说服力

• 较多人：文章被批难读、绕圈、术语解释太晚，甚至有人质疑作者写软件是否也这么糟；页眉 bug 和「说了很多又什么也没说」的观感进一步放大了反感。 > 去上写作课吧，这篇读起来很痛苦。（@lisp2240）

认为 AI 辅助 TLA+/Quint 建模能发现真实并发缺陷

• 较多人：有人在提示中要求先用 Quint 建模、确认整体无反例再实现，结果虽然慢很多，但抓出不少事务和原子性 bug；也有人让 Opus 写不变量，在集群和故障转移逻辑里拦下一个此前不可能出现、没人想到写单测的灾难性缺陷。 > 唯一抓住它的是 TLA+ 不变量，而它们也是 Opus 写的。（@lopatin）

担心把形式化交给 AI 会掩盖推理，验证链条并未真正闭合

• 较多人：有人质疑不检查自己在形式化什么，就是对智能体过度信任；更强烈的批评是，端到端证明程序正确极其困难，人类至今只能处理约一万行、且写法高度受限的程序，如果 AI 真能完成最难的部分，就不需要人类帮它做「让工具可用」这种简单部分。 > 把推理过程对人隐藏起来让我困惑；如果 AI 能完成最难的部分，为什么还需要我们帮它写工具？（@pron）

认为写出有用不变量、保持模型与实现同步才是真正难点

• 较多人：TLA+ 最适合分布式系统，但从读例子到写有用不变量仍然很难；实现与模型同步费时，AI 可能改变做法，不再坚持专用模型，而转向更贴近实现的方案。 > 从看例子到写出有用的不变量，仍然是最难的部分。（@torutofu）

认为 TLA+ 的工业落地仍有限，VLSI 是否采用存疑

• 少数人：有人贴出工业应用案例，提到 Intel 在写硬件描述前用 TLA+，但不确定这套做法是否延续，并询问如今 VLSI 行业是否还在用。

有价值的补充

• TLA+ 是用于设计、建模、文档化和验证反应式系统的形式规范语言；文中很晚才解释缩写，导致不少人读得云里雾里。
• Lamport 本人的 TLA+ 视频课程被推荐为更好的入门材料。
• 有人通过 Quint 间接使用 TLA+，把「先建模、确认无反例、再实现」写进智能体提示；也有人同时维护 Alloy 模型，但自称仍是少数派。
• Stateright 试图让验证更贴近实现代码，以减少模型与实现同步成本；还有人半开玩笑建议转向 CSP。