Write down every guarantee before you write any code

下面是一个待办事项列表做出的所有承诺。

VARIABLE tasks

Init == tasks = [i \in Ids |-> "absent"]

Add(i)      == tasks[i] = "absent" /\ tasks' = [tasks EXCEPT ![i] = "open"]
Complete(i) == tasks[i] = "open"   /\ tasks' = [tasks EXCEPT ![i] = "done"]
Reopen(i)   == tasks[i] = "done"   /\ tasks' = [tasks EXCEPT ![i] = "open"]
Delete(i)   == tasks[i] # "absent" /\ tasks' = [tasks EXCEPT ![i] = "absent"]

ClearCompleted ==
  /\ \E i \in Ids : tasks[i] = "done"
  /\ tasks' = [i \in Ids |-> IF tasks[i] = "done" THEN "absent" ELSE tasks[i]]

不是摘要。不是重要的部分。是全部。一条任务不能从不存在直接变成已完成。清空已完成项不会动未完成的项。你无法删除一个从未存在的东西。九行代码，读完之后你就读完了整个契约。

现在去找你所在系统的那个列表吧。

你找不到。它不存在。它分散在测试套件中——那些断言结果而非规则的测试，分散在处理器中的部分校验，以及最长待的那位的记忆里。这些承诺是真实存在的——你的用户依赖着每一条——但没有一个文件可以让你打开来查看它们。

这就是我想说的差距，因为你可以用一个下午来弥补它，也因为最近发生了一些变化使得弥补它变得物有所值。

素数标记和两个运算符

这就是大部分语法了，先把它过一遍。

tasks' 意思是"下一个状态中的 tasks"。/\ 是"与"。"\E 是"存在"。像 Complete(i) 这样的定义是一个公式，将当前状态与下一个状态关联起来——大声读出来：任务处于打开状态，然后它变为已完成。

就这样。大致上，这就是为此目的设计的语言。

真正的文件在你看到的这些基础上加了约八行脚手架：一个模块头，一个 TypeOK 说明任务始终恰好处于三种状态之一，还有将各个动作串联起来的两行——

Next == \/ \E i \in Ids : Add(i) \/ Complete(i) \/ Reopen(i) \/ Delete(i)
        \/ ClearCompleted

Spec == Init /\ [][Next]_tasks

Next 是"任意一个动作发生"。"Spec"是"从合法状态开始，然后只能做合法动作"。第二行比看起来更重要，我后面会再讲。

注意里面没有的是什么。没有数据库。没有 HTTP。没有提到按钮是不是蓝色的，也没有提到 UI 中的完成是否是乐观的。规格说明不是程序，也不会编译成程序——它是一个公式，说明哪些状态变化是允许的。其他一切从设计上就不在范围内，这就是为什么这个列表可以只有九行却仍是完整的。

还要注意 ClearCompleted 有两个部分：按钮只在有事已完成时才存在，而且它不会动其他任何东西。一个动作中包含两个独立的承诺。记住这一点。

这个列表很短、有限、值得争论

我预见的反对意见是：真正的系统的列表会是巨大的。

它比你想象的更小，因为这是一份规则列表，不是行为列表。行为是组合性的——这里有九种状态，而真正的系统有天文数字级的状态。生成这些状态的规则并不是。五个动作覆盖了所有曾经正确的待办事项。

这也是设计中值得争论的部分。当两个工程师对于已完成的任务是否应该允许重新打开意见不一致时，这场争论目前发生在代码审查中，在一个评论线程里，距离有人已经构建了其中一个答案之后三周。如果写成规格说明，这场争论只需要四分钟，而且发生在任何人打开编辑器之前。

这才是 AWS 结果的真正意义。他们在 2015 年把经验写成了 CACM 文章，大家引用最多的标题是关于证明系统正确性那一部分。真正可以复制的部分更安静：写规格说明在任何代码存在之前就发现了 bug——在他们最优秀的工程师已经设计和审查过的系统中。不是测试遗漏的 bug。是设计本身的 bug——通过写下保证再读回来就能发现的。

这是四十年前的技术，我们大多数人都跳过了它，因为它看起来像作业。TLA+ 是 Leslie Lamport 的；其背后的时态逻辑在 1994 年进入 TOPLOS，语言和工具在 2002 年有了专著，Lamport 在此过程中获得了 2013 年图灵奖。（值得说一下，不是为了 TLA+，人们经常搞错这个：获奖原因是逻辑时钟、安全性和活跃性、复制状态机、顺序一致性。TLA+ 是那项工作的下游，不是获奖牌的原因。）

它学术的声誉部分是实至名归的，大部分已经过时了。你不需要证明系统。不需要验证任何东西。你需要的是把保证写下来的那部分。

写这个列表一直值得做，也一直容易推迟，因为代码是由那些基本记得规则的人们缓慢编写的。

这种情况已经不再了。现在有别的东西在写代码，而且写得很快，它什么都不记得。它从未见过你系统的规则，也没有办法推断出不在它正在看的文件中的那些规则。它会写出看似合理的东西。

"看似合理"就是问题所在。看似合理的代码通过审查——这就是"我觉得没问题"的来源，而且它一直是一种诚实的坦白：审查者报告的是没有发现什么问题，因为对照完整的不变式集合进行检查从来不是选项。没有人有这份列表。

所以：写下这份列表。然后机械地、每次都对照它检查生成的代码。第二部分需要一个工具。

cargo install tlatools

一个 Rust 写的 TLA+ 解析器和求值器。不是模型检查器——它不探索任何东西。它回答关于你已有的状态的问题：

let spec = Spec::from_file("Todo.tla")?;
let eval = Evaluator::new(&spec, constants)?;

eval.holds_at("Init", &state)?;         // 合法的起始状态？
eval.step_allowed("Next", &from, &to)?; // 合法的步骤？

这个循环由三部分组成。你写列表——简短的、可争论的、几乎不变动的。AI 智能体写实现——任何语言、任何框架、任何速度。一个脚本遍历实现，对它采取的每一步都向列表提问。第三部分三十行：问实现它能做什么，然后做每一件事，记录你到达哪里，重复直到没有新东西出现。

$ ./check.py impl/correct.py
The implementation refines the specification.
9 states and 35 steps, all permitted.

九种状态是因为有两个任务，每个任务有三种状态。真正的应用有更多状态，遍历是昂贵的部分，而不是检查。

列表能 catch 住的两个 bug

这是一个 AI 智能体看似合理的 bug。完成处理器接收一个 id 并将其标记为已完成。它不检查任务是否是打开的——为什么要检查呢，按钮只出现在打开的任务上。（是按钮。不是处理器。）

这正是那种在审查中存活下来的 bug。它读起来没问题。缺失的检查在某个你没在看的地方缺失。

$ ./check.py impl/completes_anything.py
The implementation takes a step the specification does not permit.

from   a=absent, b=absent
  doing  complete(a)
  to     a=done, b=absent

The closest the specification came:
  Add(i = "a") was available, but does not produce that state,
    because tasks' = [tasks EXCEPT ![i] = Open] does not hold (1 of its 2 clauses hold)
  Complete(i = "a") was not available here,
    because tasks[i] = Open does not hold (1 of its 2 clauses hold)

第二行就是这个 bug，命名了：Complete 要求任务必须是打开的，但它不是。这是一个排序的候选列表而不是单一猜测——从此状态看 Add 也几乎符合，说出这一点比假装知道你说的是哪一个更诚实。

现在看另一个。ClearCompleted——这个有两个承诺的动作。这个实现保持了第一个而违背了第二个。它清空了整个列表：

$ ./check.py impl/clear_removes_everything.py
  from   a=open, b=done
  doing  clear_completed
  to     a=absent, b=absent

The closest the specification came:
  ClearCompleted was available, but does not produce that state,
    because tasks' = [i \in Ids |-> IF tasks[i] = Done THEN Absent ELSE tasks[i]]
    does not hold (1 of its 2 clauses hold)

"此处不可用"与"可用但不产生那个状态"。不同的句子因为它们是不同的 bug。一个是缺失的守卫条件。另一个是正确的守卫条件和错误的效果——这更糟，因为按钮看起来是能用的。你会演示它。你会交付它。有人会丢失一个他们还没完成的任务。

这个工具能区分它们，因为它知道哪个失败的子句提到了下一个状态。两种 bug 都不稀奇。两者对检查结果的测试套件都是不可见的，而两者都能被你用九行写下的列表立即命名。

用规则编写时的语言来反馈

你无法修复你无法描述的东西，模型也不行。

"测试失败了。"——再试一次。随机地。

"Expected {a: open}, got {a: absent}." — 好多了。现在从这条信息推断出规则。

"ClearCompleted 可用，但未产生该状态，因为 tasks'[i \in Ids |-> IF tasks[i] = Done THEN Absent ELSE tasks[i]] 不成立。" — 动作、条件、以及它当时所处的状态。

第三条就是一个提示。

然后我测量了它是否对 AI 智能体有帮助，结论是没有——至少没有可检测到的帮助。200 个任务，每个任务分别用无信息的重试和将失败文本反馈回去的方式各尝试一次：90.5% [85.6–93.8] 对比 92.5% [88.0–95.4]，McNemar 精确检验 p=0.125。这是一个空结果。在形式化推理子集上差距是 46.2% → 69.2%，看起来像是有什么，但 n=13 且 p=0.25，这意味着它看起来像是有什么，只是小样本经常就是这样的。

我把它报告出来是因为我跑了这个实验。这个说法的诚实状态是：机制是合理的，消息所包含的信息严格多于一个布尔值，但我没有证据表明它能提升通过率。如果你打算采纳这个做法是因为"AI 智能体在得到好的错误信息时表现更好"——先不要采纳。等你有证据再说。采纳它是因为你现在有了这份列表，而且有东西在检查它。

tlatools check 接受一个 JSON 任务——spec、states、steps、constants——并返回一个带有退出状态的裁定：0 表示满足细化，1 表示不满足，2 表示问题格式错误。

tlatools check job.json || exit 1

指向 N 个候选实现，它会告诉你哪些满足列表，对于不满足的，它会精确指出它们在何处产生分歧。如果你在生成代码、评估模型、或对基准测试评分，这是一个不需要写评分标准、不需要争论部分分的评分工具。列表就是评分标准。

第三条之所以存在，是因为仅满足细化条件也会被一个什么都不做的实现完美满足。问问我是怎么知道的。

你能信任这个检查器吗？

对任何能给你的代码打分的东西问这个问题都是合理的。

它与参考实现一致。在一个包含 39 个案例的标注语料库上——六个必须通过的实现在这里，三十三个必须被各自捕获的种子 bug——它的裁定与 Java TLC 的裁定是字节级一致的，包括三个检查中哪一个捕获了哪一个 bug。

让这个差异归零教会了我一些我原本会错误发货的东西，而这正是本文中支持精确写出保证条件的最佳论据。

记住 Spec == Init /\ [][Next]_tasks，我说过这行很重要。方括号是承重的：[Next]_tasks 意味着 Next，或者什么都没有改变。Stuttering（停顿）在每一份 TLA+ 规范中都是允许的。我之前一直在检查裸的 Next，所以任何空闲或重试的实现都会被标记为违反了规范明确允许的步骤。

修复这个问题后，一个种子 bug 存活了下来：一笔从银行账户到它自身的转账。感觉像是一次回归，直到我再次阅读规范。自我转账净值为零。它什么都没有改变。这是一个停顿步骤，而规范说停顿是可以的——所以那个实现确实满足列表，而基准测试和我在这一点上都错了。要捕获这个 bug 需要一种抽象，让操作在状态中始终可见。你不能把一个细化检查收紧到能看出状态空间没有记录的东西。

让 TLC 承担同样的 [Next]_vars 义务，它也会让那个突变体通过。两者的一致性成立；移动的是我对所写内容的理解。列表的质量取决于你对它的理解，而一个与你意见不一致的工具是在帮你。

它能读这种语言。三个公开 TLA+ 语料库中 1,258 份规范里的 1,256 份：examples 仓库、community modules 以及 TLA+ tools 自己的测试套件。它读不了的两份也是官方解析器 SANY 读不了的两份。这些文件每一个是如何被读的记录在 golden/ 中，所以一个改动能说出它改动了哪些文件，而不是仅仅移动了一个数字。

它以无聊但可靠的方式被检查过。166 个测试，clippy-pedantic 清理通过，以及一个鲁棒性套件，馈送每个 fixture 的每个前缀和每行被丢弃的行——因为一个在半保存文件上就会 panic 的解析器是一个你没法放进循环里的解析器。tla-syntax 和 tla-eval 完全没有外部依赖。

TLC 是 TLA+ 自带的模型检查器。它做的是探索：从你的初始状态，应用每一个动作，遍历可达状态空间寻找违规。当你正在设计一个协议、还不知道你的系统能做什么的时候，这是正确的问题。

在这里你已经有了实现，所以问题不同了——这些步骤，代码刚刚采取的这些步骤，是否被列表所允许？

TLC 可以回答这个问题。我想说得精确一些，因为我在之前的草稿中这一点是错的，有人会抓住它：你可以把步骤编码为数据，写一个普通的安全不变量来断言每一步都是使能的，然后运行检查器。没有活跃性属性，没有工程化的故障。在 to-do 规范上它在 0.78 秒内找到坏步骤。有已经发表的论文在正确地做这件事——Cirstea、Kuppe、Loillier 和 Merz 的《Validating Traces of Distributed Programs Against TLA+ Specifications》，Kuppe 维护着 TLA+ tools。如果你想在生产系统上做 trace 验证，从那里开始。

剩下的范围更窄，但更真实。TLC 告诉你这个步骤是非法的，但不告诉你哪个合取式失败了。而且那 0.78 秒几乎全是 JVM 启动和 SANY 解析，每次查询都要再付一次——跑一次可以，在每个 AI 智能体编辑后都跑的循环里就不行了。

结构化的 blame 而不是布尔值，延迟低两到三个数量级。这就是它的卖点。这些是组合关系，不是竞争关系。

它不是模型检查器。如果你想知道你的系统能到达哪些状态，用 TLC。

它不验证你的程序。它检查你交给它的那些转换。如果你的遍历漏掉了一条路径，没有东西会检查那条路径。

你的列表可能是错的。它是你争论的东西，而不是什么是真的。我本来可以把 ClearCompleted 写成清除所有东西，然后那个"有 bug"的实现就会是正确的。列表简短可读是唯一的防御，这就是保持它简短可读的理由。

整数是 64 位的，实数运算没有实现，时间公式会被拒绝而不是被猜测，TLAPS 证明会被跳过。

git clone https://github.com/copyleftdev/tlatools-rs
cd tlatools-rs
cargo build --release
demo/todo/check.py demo/todo/impl/completes_anything.py

整个演示在 demo/todo——上面的规范、三个实现、以及检查它们的脚本。CI 在每次 push 时运行它，所以如果你拿到的时候它坏了，那是 bug，我很乐意听到。

crates: tlatools · tla-eval · tla-syntax · tla-oracle

source: github.com/copyleftdev/tlatools-rs

docs: docs.rs/tla-eval

如果你有一个 TLA+ 文件它读错了，这是你能发给我的最有用的东西。

从一个开始。挑选你系统中一个错误的状态变更会真正造成伤害的部分——钱、权限、那个没人完全信任的状态机。写下它被允许做什么。会花一个下午，而且它会比你预期的短。

你会在写的过程中发现一些东西。每个人都会；这就是 AWS 的结果，而且它并不微妙。然后你就会有那个文件——你当前工作的任何系统都不存在的那个文件——之后所有写出来的东西，无论是你写的还是机器写的，都可以对照它来检查。