Teiva Harsanyi 用 TLA+ 形式化验证 Barista 系统并发现测试遗漏的真实缺陷

Teiva Harsanyi 2026年11月12日 1 分享 ☕ 欢迎来到 The Coder Cafe！Building Barista 的第一部分讲了架构。今天我们通过一个我的测试没抓到的真实 bug 来探索形式化验证。你会了解什么是模型检查、怎么读懂一点 TLA+，以及它为什么能抓到我们根本想不到的 bug。我在 Google 花了很多时间在形式化验证上；这一次，我把它指向了我自己的系统。找个舒服的姿势，来杯咖啡，我们开始吧！

一天一封邮件 简单概括一下 Barista：它是我构建的一个系统，会抓取数百个来源，为每个用户生成独一无二的提示词，然后每天给该用户发一封邮件，里面是为你挑选的最佳来源。

确保 Barista 每个用户每天只发一封邮件，对我来说很重要。如果 Alice 在随便哪一天收到两封相同的邮件，那是极其糟糕的用户体验。

正如第一部分所讨论的，Barista 是一组通过 Postgres 协调的独立阶段。最后一个阶段 Send 每 5 分钟运行一次，找出那些发送时间已过的用户，并把他们被 Rank 阶段选中的文章通过邮件发出去。

Send 阶段启动，发现有封邮件要发给 Alice。 Barista 调用邮件服务商，收到一个 ACK。 ✅ Barista 在 Postgres 中写回：当天发给 Alice 的邮件已发送。 Send 阶段启动，发现有封邮件要发给 Alice。 Barista 调用邮件服务商，收到一个 ACK。 ❌ 在写回 Postgres 说邮件已发送之前，Barista 崩溃了。 Send 阶段再次启动，发现有封邮件要发给 Alice。 Barista 再次调用邮件服务商，收到一个 ACK。← 重复邮件 ✅ Barista 在 Postgres 中写回：当天发给 Alice 的邮件已发送。

怎么防止这种情况？我专门为此挑选了邮件服务商：Plunk。为什么选 Plunk？因为它接受幂等键。

调用 Plunk 时，我会传一个类似 alice-20260520 的键：用户加日期。如果 Plunk 再次收到相同的键，它什么都不发；它回复一个 409。我的代码把这个 409 读作“这些文章已经发过了”，并把它们标记为已发送。没有重复。

这是一个有意识的决定。Plunk 每封邮件的价格是 AWS SES 的 10 倍，而后者没有幂等键。我很乐意为此付费。

一个业务决策：不允许重复，哪怕成本更高。 一个合理的设计，由邮件服务商替我做去重。 单元测试、集成测试、端到端测试。全部通过。 对代码有很好的心智模型。纯粹的智力掌控。

现在，如果我告诉你我的代码里有个 bug 呢？一个我的测试全都没抓到的 bug。我只用了一种叫形式化验证的东西才把它找出来。我们来看看是怎么回事。

形式化验证 在成为 SRE 之前，我从事空中交通管理（我在 Reliability Explained 里聊过）。这是一个所谓的安​全关键领域。原因你很容易想象。

在安全关键的系统中，测试全绿是不够的。这正是智力掌控的盲区：测试只检查我们想到过的场景。而真正伤人的 bug，按定义就是那些我们没想到的。

在这类领域中，测试全绿并不是对话的终点。有些团队会走得更远，去证明某些 bug 不可能发生。例如，Airbus 使用了一个名为 Astrée 的静态分析器，证明 A340 和 A380 的飞行控制软件不存在一整类运行时错误。

那么，与其一个一个地挑选场景，如果我们能检查所有场景呢？这就是形式化验证背后的理念：精确地描述系统，写下它必须遵守的性质，然后让工具检查没有任何可能的执行会破坏它们。

注意这个词：验证（verification）。它回答的是“我们有没有把东西做对？”，意思是设计是否遵守了我们的性质。不要和确认（validation）混淆：“我们有没有做对的东西？”，意思是这些是否是我们真正需要的性质。工具能做第一件事。第二件事仍然得靠我们自己。

验证一个系统有几种方式，从数学证明到在生成的输入上运行真实代码。我用的那种叫模型检查。

模型检查器把系统看作状态（每个变量的一个取值）和动作（从一个状态到下一个状态的一步）。它从初始状态出发，尝试每一个可能的动作，再从每个新状态尝试每一个可能的动作，以此类推，直到访问完所有可达状态。测试只走一条路径。模型检查器走遍所有路径。

这就是为什么它能找到没人会写测试去覆盖的 bug。AWS 在 2015 年的一篇关于他们如何使用形式化方法的论文中描述过：他们的一个 DynamoDB bug 挺过了设计评审、代码评审和测试。触发它的最短事件序列长达 35 步。

在每个状态，模型检查器都会检查我们的性质。性质分两种：

安全性：坏事永远不会发生（例如，Alice 永远不会收到同一封邮件两次） 活性：好事最终会发生（例如，Alice 最终会收到她的每日邮件）

当某个性质被破坏时，我们会得到一个反例：导致那里的确切步骤序列。

我用的模型检查器是 TLC。它读取用 TLA+ 编写的模型，TLA+ 是 Leslie Lamport 创建的一种语言，用来把系统描述为状态和动作。换句话说：我们用 TLA+ 描述系统，TLC 探索它能到达的每一个状态。

TLA+ 规约看起来不像代码。没有一条接一条执行的指令。相反，每个动作都是一个公式，它说明两件事：这一步何时被允许（对当前状态的条件），以及这一步之后状态是什么样（下一个状态中的取值）。然后 TLC 按每一种可能的顺序尝试每一个被允许的动作。

看懂下面的例子，几个符号就够了： x' 是 x 在下一个状态中的值 \A 和 \E 表示“对所有”和“存在”

我们用一个简单的例子来看看。想象一家咖啡馆只剩一个可颂，有两个咖啡师。当顾客要一个可颂时，咖啡师做两件事：首先，他们查看展示柜里是否还剩一个；然后，把它卖出去。

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）