分布式系统（E06）：从 PlusCal 反例到 IronFleet 证明边界

测试只能覆盖运行过的执行，论文证明也不自动约束实现。形式化方法的价值，在于把“系统应该做什么”“允许哪些环境行为”“代码怎样实现协议”分别写成可审查对象，再给它们建立明确的连接。连接少一段，工具显示绿色也可能只证明了另一个问题。

分布式系统（E05）：NOPaxos、Streamlet 与 HoneyBadger 的假设边界

四类对象不能混称为“已经证明”

一项可核验的形式化工作至少包含规格、模型、性质和证据。生产实现通常还需要一条从代码到规格的证明链。

flowchart LR
  R[需求与环境假设] --> S[高层规格]
  S --> M[有限模型]
  M --> C[TLC穷举/反例]
  I[实现代码] --> P[协议状态机]
  P --> S
  I --> V[实现级证明]
  V --> P

TLC检查的是给定模型是否满足指定性质。若规格漏掉一种失败，或者常量把系统缩得过小，穷尽状态也不会补上缺失的世界。IronFleet则继续处理实现到协议的距离，但仍保留规格、验证器和运行平台组成的可信计算基。

TLA+把执行写成状态序列

TLA+中的state是一次变量赋值，step连接前后两个状态，behavior是无限状态序列。action可以同时约束未加撇号的旧变量和加撇号的新变量。一个常见规格形状是：

Init /\ [][Next]_vars

Init限定初态，Next列出合法状态转换；方括号形式还允许vars不变的stuttering step。stuttering使内部实现可以多走若干对高层不可见的步骤，也使活性讨论不能只看“是否还有业务动作”。

本篇锁模型只有两个客户端。状态由owner和每个客户端的phase组成，网络、崩溃、持久化与多轮请求均未建模。

stateDiagram-v2
  [*] --> idle
  idle --> waiting: Request
  waiting --> held: owner为空且原子授予
  held --> done: Release
  done --> [*]

安全性质MutualExclusion要求任意状态最多一个客户端处于held。类型不变量TypeOK约束变量值域。两者都是state predicate；检查不变量，实质是在所有可达状态上检查它们。

PlusCal的label决定原子边界

PlusCal算法放在TLA+模块的注释中，由pcal.trans翻译成Init、Next、程序计数器和各label对应的action。label不是排版符号，它决定一次原子步骤能跨过哪些语句。

正确规格把检查空闲和写入持有者放在同一个Acquire步骤：

Acquire:
  await owner = "none";
  owner := self ||
  phase[self] := "held";

变异规格把它拆成CheckFree和GrantWithoutRecheck。两个客户端都可能先观察到空闲，再分别写入：

sequenceDiagram
  participant C0 as Client 0
  participant C1 as Client 1
  participant L as Lock state
  C0->>L: CheckFree，owner=none
  C1->>L: CheckFree，owner=none
  C0->>L: GrantWithoutRecheck，held
  C1->>L: GrantWithoutRecheck，held
  Note over C0,C1: MutualExclusion违例

这个反例不依赖线程真的同时执行。状态机只需找到一种合法交错：两个检查都发生在任一写入之前。把代码里的“先读后写”错误压成一个原子动作，会从模型中删除最重要的竞态。

实验：两个独立有限模型给出同形结果

实验固定TLA+ Tools v1.7.4。JAR自报TLC 2.19（2024-08-08）和PlusCal translator 1.11（2020-12-31）。所有下载、翻译产物、日志和Java临时文件都在examples/distributed-systems/.build/e06/。

mkdir -p examples/distributed-systems/.build/e06/tmp
export TMPDIR="$PWD/examples/distributed-systems/.build/e06/tmp"
export TMP="$TMPDIR" TEMP="$TMPDIR" PYTHONDONTWRITEBYTECODE=1
python3 -B examples/distributed-systems/formal-e06/check.py \
  --output examples/distributed-systems/.build/e06/observations.json

Python 3.12.3模型穷尽正确模型的15个状态，没有发现互斥违例；变异模型访问24个状态，在6步后找到可重放反例。它还保留一个持续stutter的lasso：请求已经等待，授予动作持续可用，但调度永远不选择它。

PlusCal源在.build/e06副本中翻译，再用单worker运行TLC。正确规格检查21个不同状态，TypeOK、MutualExclusion以及弱公平下的Termination均通过，退出0。变异规格在状态图第7层报告双方同时held，退出12。两种模型的状态数不同，因为PlusCal翻译包含程序计数器和Critical步骤；本文没有证明两者等价。

首轮TLC语义分析还拒绝了遗漏Naturals扩展的规格，因为<=没有声明。PlusCal翻译成功只说明算法能生成TLA+文本，SANY语义检查、TLC性质检查仍是后续独立关口。

完整轨迹见观察结果，运行版本和命令见实验证据，验证范围见验证说明。

安全性、活性与公平性分开写

安全性回答“坏事是否发生”。互斥违例只需一个有限前缀：从初态走到两个held，反例已经成立。活性回答“好事是否最终发生”，必须约束无限行为。

flowchart TD
  W[客户端处于waiting] --> E{grant是否持续enabled}
  E -->|否| B[先检查阻塞原因]
  E -->|是| F{是否假设弱公平}
  F -->|否| S[允许无限stutter]
  F -->|是| G[该动作不能永远被跳过]
  G --> D[最终进入done]

本篇fair process让翻译后的Spec包含每个客户端动作的弱公平条件。它排除“动作从此一直可用却永不执行”的调度，却不提供固定完成时间，也不自动表示网络最终同步。若加入消息、崩溃和重试，必须分别建模消息丢失/重复/重排、持久状态、恢复动作和客户端身份；把这些行为省略掉，就不能声称已经验证相关故障。

超时也应进入规格。客户端没收到回复时，服务端可能尚未执行、已经执行但回复丢失，或处在恢复中的未知状态。若模型只有调用和成功返回，超时语义、请求去重和恢复后的结果查询都不在证明范围内。

TLC的“穷尽”有明确边界

TLC是显式状态模型检查器。常量Clients = {c0, c1}把本篇系统限制为两个一次性请求者；模型没有网络、磁盘和进程重启。21个不同状态被穷尽，只能推出这个有限实例内、这份规格下没有找到违例。

还需记录工具本身的版本边界。TLA+ Tools v1.7.4修复了一个多worker活性检查可能漏报违例的问题，因此本篇固定v1.7.4并用单worker。64位state fingerprint仍存在非零碰撞风险，模型约束、对称化和抽象也可能隐藏行为。正式验证报告必须把工具版本、参数、状态数和未建模项一起保存。

可迁移的检查方式是“先造一个应该失败的变异”。若删除原子边界后TLC仍显示通过，可能是性质、动作或检查配置没有连上。反例不是失败的附属品，而是规格能观察目标错误的证据。

IronFleet把证明推进到实现

IronFleet的高层结构有三层：集中式服务规格、抽象分布式协议、每台主机上的命令式实现。协议到规格使用TLA-style state-machine refinement；实现到协议使用Dafny中的Floyd–Hoare式验证。

flowchart TB
  HS[集中式高层规格] <-->|refinement mapping| DP[抽象分布式协议]
  DP <-->|Dafny/Hoare证明| HI[每主机实现]
  ENV[网络与调度假设] --> DP
  TCB[规格/验证器/编译运行平台] --> HS
  TCB --> HI

IronRSL的高层安全规格把服务行为约束为确定性应用的顺序执行，并证明协议与实现细化它。项目issue #3还给出一个重要边界：删除回复缓存后原规格仍可验证，因为exactly-once没有写进高层规格；线性化与请求去重不是同一性质。活性定理另有条件：存在存活多数派，客户端持续重发，相关节点之间最终出现有界网络延迟，调度器获得最低执行频率，时钟误差和资源使用不越界。它不是任意异步网络中的有限时间保证。

实现事件处理并非天然原子。IronFleet用reduction论证把细粒度执行重排为抽象主机步骤，Dafny检查支持reduction的实现义务；论文也明确说明，“这些义务足以推出reduction”的连接只有非形式化证明草图。证明链比只检查模型更长，但没有因此变成无假设。

可信计算基还包括高层规格、短主循环、Dafny、编译器和运行时、操作系统及硬件。论文代码没有崩溃恢复，也没有验证客户端库；IronRSL没有成员重配置。后续仓库加入的网络安全和新版工具依赖不能倒推成2015年论文已经证明的性质。

工程上怎样选择验证层级

目标	合适证据	仍需补的部分
找协议状态机中的竞态	PlusCal/TLA+与TLC反例	模型覆盖与抽象审查
检查有限参数下的不变量	TLC穷尽结果	参数推广或归纳证明
证明协议细化高层规格	refinement证明	规格与环境假设审查
证明实现遵守协议	Dafny/Hoare逻辑等	编译、运行时、I/O和TCB
证明生产服务可靠	形式化证据加测试、故障演练和运维证据	真实部署与持续变更

模型检查适合快速找到短反例，也适合在设计阶段固定原子边界。实现级证明能缩短协议与代码之间的距离，但证明注解、求解器稳定性、可信组件和功能限制都会形成持续成本。二者不是替代关系。

两个推演练习

把客户端数从2改成3，正确模型仍通过，是否证明任意客户端数都互斥？

不能。它只扩大了一个有限实例。要得到参数化结论，需要归纳不变量或其他能覆盖任意规模的证明，并检查抽象是否保持所需行为。

模型加入弱公平后Termination通过，能否承诺请求100毫秒内完成？

不能。弱公平只排除持续可用动作被永久跳过，没有给出时间上界。有限时延SLA需要时钟、网络、调度和资源上界，并在实现与部署层验证。

E07转向真实控制面：Kafka KRaft、Kubernetes/etcd和HBase/ZooKeeper都使用共识或协调服务，但控制面元数据与业务数据面的复制不能混为一层。

参考资料

• Lamport，Specifying Systems。
• Lamport，The PlusCal Manual与The PlusCal Algorithm Language。
• TLA+ Foundation，TLA+ Tools v1.7.4与TLC文档。
• MIT 6.5840，Verification: IronFleet。
• Hawblitzel等，2015，IronFleet: Proving Practical Distributed Systems Correct。
• Microsoft，IronFleet论文版本代码说明。
• Microsoft Ironclad，Issue #3：exactly-once不在原规格内。