一句话定义：TLA+（Temporal Logic of Actions，动作时序逻辑）是一门用来描述系统"应该怎么运转"的形式化规约语言。写出的规约交给模型检验器 TLC，它会穷举所有可能的状态和事件顺序，把死锁、竞态、丢消息这类设计漏洞连同一条可复现的路径一起交给你。它由 Leslie Lamport 提出，主要在分布式系统领域使用。
原理：不是跑一遍，而是把所有走法都走一遍
拿会议室预约打个比方。规则听起来毫无歧义："谁先点谁订上。"但两个人几乎同时点击时会怎样？TLA+ 的做法是：先把"人、会议室的占用状态、点击事件、状态之间的转移条件"写成一台状态机，再让 TLC 枚举所有可能的交错顺序——A 先点、B 先点、同时点、点了没收到回执又点一次……只要存在一条路径能让两个人都以为自己订成功了，它就把这条路径打印出来。这是"穷举搜索反例"，和单元测试、压测抽查几条路径完全不是一回事。想要更接近伪代码的写法，可以用 PlusCal，它会编译成 TLA+。
和 Lean 4 差在哪
| TLA+ / TLC | Lean 4 | |
|---|---|---|
| 想回答 | 这个设计有没有反例 | 这条命题能否被证明 |
| 方法 | 枚举有界状态空间，自动找错 | 人机交互构造证明，机器核验 |
| 交付物 | 一条出错的执行路径 | 一个不可反驳的证明 |
| 典型对象 | 分布式协议、并发算法、多智能体流程 | 数学定理、算法正确性证明 |
| 成本 | 建模抽象费功夫，跑起来基本自动 | 证明工程重，需要人工引导 |
关键差别在于：TLA+ 给你的是"有限范围内的反例搜索"，找不到反例不等于正确——状态空间会爆炸，必须靠抽象取舍；Lean 4 给你的是全称证明，代价是门槛高、且得先有精确定义。两者不是替代关系，更像"先用便宜手段找错，再用昂贵手段证明对"。
为什么 AI 圈突然重提它
因为 agent 系统本质上是并发系统：多个角色同时读写同一份状态，中间还夹着重试、超时、消息乱序、工具调用失败。提示词管不住并发——你没法用自然语言保证"不会重复下单"。而把协作流程写成状态机规约，交给 TLC 穷举，就能在写代码之前发现设计事故。LLM 可以帮忙起草规约草稿，但草稿接不接受由检验器说话，这构成一个干净的"生成—检验"闭环。
对普通人的意义
不必人人都去学。但如果你的系统里存在"多个角色同时动一份状态"，值得知道有这条路：先把流程画成状态机，再问一句"所有交错顺序都安全吗"。具体语法与工具细节以官方页面为准。