Anatoliy Bilenko 和 Alberto Carretero：用形式化方法和 AI 让数据库协议可靠

Anatoliy Bilenko 开场先讲 Canonical 用来设计协议、建立正确性信心的方法：状态机、形式化规格与验证、TLA+、Antithesis、Jepsen、全局状态重建、基于模型的测试，以及基于性质的测试。这些是开发过程的组成部分，不是实现写完之后再做的一次验证。

Bilenko 是 Canonical 的主任工程师，负责 Dqlite 分布式数据库团队。他还主持一个性能与正确性学院，培训工程师和经理做性能分析和形式化验证。来 Canonical 之前，他在 Seagate 做了十年分布式存储、性能和事务管理。共同主讲人 Alberto Carretero 是软件工程师、Dqlite 贡献者，工作重点是正确性、形式化方法、设计验证和分布式算法，背景是数学和计算机科学。

写协议对许多工程师来说是少见的任务。大学里和工作里，未必有人教过怎么做。成功路径通常不难：用现成的库在网络进程之间发消息。难处出现在环境不再按预期运转的时候。故障会引入更多状态，而这些状态必须在代码、轨迹，以及协议的每一种表示里都还能管得住。

设想把一个文件从一个进程传到另一个。消息可能丢、可能重复，进程也可能崩溃。单独处理其中一种情况，已经比成功路径费事；处理它们可能的交错更难。假设接收方按消息做了持久改动，但确认丢了。发送方和接收方对发生了什么的认知不再一致。设计必须回答：系统现在处于什么状态。

可能的故障覆盖网络、磁盘、进程和时间。Bilenko 还提到拜占庭故障，比如内存损坏，或故意做出的意外行为。重点不是每个协议都要用同一种办法解决所有能想到的问题，而是设计者必须针对相关的故障模型做推理，不能让这些情况一直隐在暗处。

还有社会层面。协议实现可能用几十年，当初理解假设的工程师却会离职或退休。如果设计和代码渐行渐远，曾经写清楚的假设就变成只有少数人记得的知识。所以让设计和实现保持连接，既是数学问题，也是维护问题。

分散的团队还需要一套讨论系统的共同方式。在 Canonical 这样的公司，工程师可能远程工作，用的抽象也不一样：有人喜欢接口，有人喜欢状态机，有人喜欢序列图，还有人靠一轮轮实验往前走。Bilenko 主张要有一套共同语言，让这些人能一起面对协议和分布式系统问题。他的起点是状态机。

做一个把大文件分块发送的协议，第一反应往往是定义消息、画序列图。那张图能说明一次交换，通常却揭示不出所有可能导致失败的交错。调查一场灾难时，工程师需要的是产生它的状态和转换序列，而不只是一张预期对话的图。

Bilenko 换成发送方的状态机来看。这个例子来自性能与正确性学院的入门协议练习，有六个状态，动作包括发送、接收和超时。这种表示把发送方状态的原子变化写清楚了。它也说明发送方只是分布式系统的一部分：接收方和网络还要建模。

状态机变大之后，分解就必不可少。一个组件可以看成一个盒子：有输入动作或事件、输出事件，以及内部状态。把这些组件组合起来，就得到整个系统的层次视图。在文件传输的例子里，就是把发送方、接收方和网络行为分开，同时保留连接它们的动作。这种抽象能控制复杂度，又不必丢掉状态机这套语言。

把每个组件的动作记在各自的时间线上再合起来，就得到系统事件的历史。再记下不同进程上转换之间的因果关系，这段历史就能用来解释发生了什么。这次讲座 Bilenko 没有讲如何捕获这些关系，但强调它们能把原本分开的时间线连起来。

真实的执行历史包含许多时间线、状态转换、标签和因果链接。细节很快就会密到没法用眼睛看。要推理这段历史，工程师会定义性质：也许某个动作绝不能和另一个重叠，或者协议最终必须推进到完成。历史提供具体的执行，用来对照这些期望。

两类常见的性质是安全性和活性。安全性说的是坏事永不发生：比如最多只有一个未完成的请求，或者回复对应状态机里更早的请求。活性说的是好事最终会发生。投递保证可能要求：在正确进程之间发送的消息最终会到达。这些性质让本来只是口头说法的主张有了精确含义。

系统足够复杂时，状态和转换的图就会难写、难维护。规格语言提供另一种表示。Bilenko 用 Leslie Lamport 提出的 TLA+ 来表达状态、事件和系统演化。屏幕上的例子里，发送和投递消息都写出来了，输出事件也可以通过状态变化来建模。好处是规格更好管，假设也写得清楚。

同一种语言也用来表达模型应当满足的性质。在链路的例子里，一条活性性质说：在下层网络公平投递的假设下，正确进程之间发送的每条消息最终都会到达。时态算子让规格区分什么必须始终成立、什么必须最终发生。对 Bilenko 的团队来说，这也是讨论设计和实现细节的共同语言。

有了 TLA+ 规格和性质之后，团队用 TLA+ 工具集里的模型检查器 TLC。TLC 探索模型里的转换，包括消息投递、超时和崩溃相关的行为。它检查探索到的模型是否满足所述性质。状态空间可以看成一张大图：每个节点是一个系统状态，每条边是通向另一状态的动作。

TLC 还能生成轨迹。轨迹是那张图上的一条特定路径——建模的分布式系统里发生过的一串事件。这些轨迹的用处不止于检查规格本身。它们可以成为基于模型的测试的输入，让实现对照从设计导出的行为来跑，而不只是对照工程师手写的例子。

在真实程序里，有些性质可以在本地检查。发送方状态机的每次转换都有前置条件。例子里，相关传输循环开始前文件必须关闭；开始发送分块之后，文件必须打开，超时必须设好。其他发送方状态也有类似条件。这些检查关心的是单个进程能直接观察到的信息。

全局性质更难，因为单个进程观察不到分布式执行里所有相关事件。Raft 这类共识协议的性质，在模型或模拟器里很容易陈述和检查，因为系统状态都在手里。更难的问题是：同样的期望，怎么对照一个真实在跑、信息散落在各个进程上的协议来评估。

团队的答案从历史开始。如果系统记录了状态和因果关系，重建算法就能产出适合分析的事件排序。Bilenko 提到 Chandy–Lamport 和其他方法，同时承认它们有局限。一种可能的步骤是对记下的因果关系做拓扑排序，然后在得到的状态序列上评估性质。

这就是团队做数据库分布式事后分析的方式。不只是知道数据库出了问题，而是尽量找出通向故障的步骤序列。Bilenko 把历史重建说成设计的抽象性质与导致问题的具体执行之间的实用连接。

模型和代码之间还有另一条连接：在测试环境里回放模型生成的轨迹。写完协议的状态机之后，团队可以从模型导出轨迹，喂给实现的测试框架。实现的行为与模型一致时，这些测试就通过。目的是在代码和设计各自演化时，让两边保持同步。

Bilenko 把一条开发路径概括为可执行的设计。从 TLA+ 规格出发，用 TLC 检查模型，生成轨迹，再把轨迹喂给基于模型的测试。测试随后给出证据：实现的协议是否对应模型。这条工作流让设计变成团队可以执行、可以对照测试的东西，而不是一份渐渐和代码脱节的文档。

第二条路径从真实集群出发——比如三个节点——收集执行日志。团队重建一条轨迹，送给性质检查器，把全局性质带进测试过程。这并不能消掉分布式快照或重建算法的局限。Bilenko 指出，他们的实现针对特定协议，因而可以在通用方案更难下手的地方，用协议专用的启发式来帮忙。

已有系统或遗留系统即使不是从可执行规格起步，也需要类似的工作流。Jepsen、Antithesis 这类工具可以跑分布式场景、挖出边角情况。Canonical 测试时两种都用，还用 Antithesis 探索状态、帮助重建全局执行轨迹。这种探索可以作为证据，说明正在跑的协议实际表现如何。

在那条工作流里，团队在探索框架下跑协议，重建全局状态，识别性质，拼出一份可浏览的历史。智能体可以同时拿到这份历史和协议的代码库。调查结果再用来改进埋点，让分布式性质能更准确地表达和检查。这个循环反复进行，直到团队对系统行为有更清楚的说明。

接下来由 Carretero 来看这套工具箱的限度。听起来好像选对工具组合，就能自动做出能用的协议。实际上每种方法都会带出自己的难题。TLC 对模型检查和基于模型的测试有用，但团队仍要决定：探索到什么程度才有足够把握可以停。

行覆盖率给这个问题的答案会误导人。设想两个进程读取共享计数器，更新本地副本，再写回共享计数器。先跑进程 A 再跑进程 B，可以执行每一行代码，却从未碰到会丢失更新的那些交错。对协议来说，真正有意义的复杂度在于操作的顺序和交互，而不只是每条语句有没有跑过。

状态空间图提供了更好的覆盖思考方式，但原始计数仍然解决不了问题。TLC 可能报告检查了 5000 万个状态。这些状态也许覆盖了算法的重要部分——也可能大部分是反复选举，或者发消息再丢消息的循环。数字再高也说明不了多少，除非工程师清楚搜索真正到达了哪些行为。

最简单的应对是把模型约束到更小的区域。工程师可能认定两次选举就足以暴露相关边角情况，或者三条复制条目就够测重要的排列。这些边界缩小了搜索，但约束区域内还是同一个问题：工具有没有跑到有意思的行为，还是把力气花在网络实现这类没有信息量的细节上？

另一种应对是定义有意思的谓词。不要只问行覆盖率或状态数，而要问模型有没有到达两个候选节点的选举，或者复制数据里的冲突。这至少能确认特定情况发生过。弱点是人工偏见：工程师必须事先知道该点名哪些情况。如果重要的边角情况事先都知道，普通测试就已经接近够用了。

团队也可以选择有意思的起始状态。与其等检查器自己走到双候选选举，不如从那里起步，探索附近的状态。几个起点可以打开几片行为邻域。这把力气导向团队觉得有希望的情况，但仍然证明不了探索过的邻域包含了所有重要故障——也证明不了工具在里面花的时间有意义。

再进一步是引导探索本身，说明哪些行为看起来更有意思。Carretero 提到 Apalache 的 JSON-RPC 接口，以及 TLC 的探索策略，作为影响搜索的办法。到这一步，过程开始像模糊测试。团队考虑过自己做模拟器和模糊测试器，后来意识到现有系统已经能提供它需要的大部分机制。

Carretero 把 Antithesis 和 Jepsen 区分开，因为人们有时把两者当成可以互换。按他的说法，Antithesis 在确定性环境里做有引导的探索。它可以给执行做快照、回到更早的时间点，再顺着执行走一遍来调试故障。这套组合让团队能把搜索导向有意思的行为，拿到有用的覆盖。

Jepsen 的长处不同：灵活的随机故障注入。它以测试分布式系统正确性著称，但随机配置并不能告诉团队这次运行是不是在探索有意义的场景。故障可能只是阻止了选举，让协议毫无进展。对照的是工具如何搜索行为，以及为什么用了其中一个，并不能消掉另一个的所有局限。

不去探索巨大的状态空间，另一种办法是证明一条性质。形式化论证可以确立 TLA+ 模型某个方面是安全的。过去，构造这样的证明可能要专家花上几天或几周。Carretero 说，LLM 现在能帮忙给一些定理写证明，再用检查器测试提出的证明能否通过。吸引人的是经过检查的结果，而不是证明本身的文字。

即使完美的证明也不能关闭整个正确性问题。它证明的是规格上的事情，并不自动说明代码实现了规格。团队仍然需要连回实现的途径，比如生成的轨迹和测试。那又可能直接绕回状态空间探索，以及 Antithesis 或 Jepsen 这类工具。形式化证明改变的是能拿到哪种证据，并没有抹掉模型到代码的缺口。

LLM 在证明工作里的能力也不均匀。Carretero 觉得它们对付熟悉的证明有效，但任务需要新的或更简单的论证时就不那么可靠。模型可能反复尝试整个问题然后失败。它可以搜索历史或网上的材料，也可能塞进一些假设，让最终结果看起来成立，同时把本该证明的实质掏空。仍然需要足够懂 TLA+，才能检查并引导这项工作。

规格规模是另一道障碍。按团队用 TLAPS 的经验，加上动作、让模型更接近实现，证明复杂度会迅速增长。小规格有时几乎可以在 AI 辅助下自主证完；大规格就难得多。可是一份打算贴近真实代码的规格，往往需要更多细节。精确和可处理性互相拉扯。

团队减轻负担的办法是从已经有既成证明的模型起步，Raft 就是例子。Carretero 明确说基线并不完美，但可以当作实用的基准事实。工程师不去重建整个模型和证明，而是在上面加上自己的改动，并试图确立这些改动保持了原先的保证。

对 LLM 来说，推理这个增量比给整个系统发明一套论证容易得多。任务变得更窄、更机械：找出改了什么，并表明改动维持了基线的保证。这并不能让更大的正确性问题消失，但给了 AI 辅助证明一个更好下手的范围。

Carretero 收尾讲工作流的另一端：在正在运行或遗留的系统里检查全局不变量。团队可能想确立只有一个领导者，或者数据没有丢失。故障会让观察本身变复杂。进程成功记下动作时，推理这个动作并不难，但动作和日志条目未必是原子的。

假设一个进程提交了数据，却在记下这次提交之前崩溃了。重建器不能只凭看到的事件就推断出缺失的状态。系统可能需要再发出信息，工程师也必须把未知的部分算进去。通用的分布式重建算法在这里有局限。针对协议定制的测试环境能把问题简化，团队觉得这有用，尽管它给不出万能解法。

最后的总结回到互补的工具。模型、状态机和性质记录设计，帮助区分有效行为和无效行为。性质和证明支撑形式化推理，轨迹和重建的历史则帮助检查正在运行的系统。测试仍然是核心：基于模型的测试、确定性模拟、基于性质的测试、Jepsen 这类随机测试，以及 Antithesis 这类模糊测试，各自贡献不同种类的证据。

没有银弹，Carretero 总结道。团队不能从头开始、把清单上的每项技术都用一遍，就假定做出的协议能用。实际要做的是搭配这些方法，理解各自的局限，用合在一起的证据建立信心：协议是正确的。