Page 309 - 《软件学报》2026年第5期

2188 软件学报 2026 年第 37 卷第 5 期

1 (* 模型配置常量 *)

2 CONSTANTS Servers, MaxCrashes, MaxEpoch
3 CONSTANTS LOOKING, NOTIFICATION_MSG, FOLLOWERINFO_MSG
4
5 (* 变量 *)
6 VARIABLES role, messages, epochLeader
7
8 (* 系统行为 *)
9 HandleMsg == \E m \in messages:
10 CASE m.mType = NOTIFICATION_MSG -> HandleNotMsg(m.dst, m)
11 [] m.mType = FOLLOWERINFO_MSG -> HandleFInfoMsg(m.dst, m)
12 [] OTHER -> Assert(FALSE, "Error: unknown msg")
13
14 (* 环境行为 *)
15 NodeCrash == \E s \in Server: Crash(s)
16
17 (* 正确性属性 *)
18 LeadershipInv ==
19 \A epoch \in 1..MaxEpoch: Cardinality(epochLeader[epoch]) <= 1
20
21 (* 初始状态和状态转移 *)
22 Init ==
23 /\ role = [s \in Server |-> LOOKING]
24 /\ epochLeader \in [1..MaxEpoch -> SUBSET Server]
25 /\ messages = [s \in Servers |-> [d \in Servers \ {s} |-> <<>>]]
26
27 Next == \/ HandleMsg \/ HandleTimeout \/ ClientRequest
28 \/ NodeCrash \/ NodeStart
图 8 TLA+ 规约内容概要

5.1.2 规约的定位
规约作为对目标系统的抽象, 其系统行为规约可根据定位和使用场景分为高层次规约和低层次规约. 高层次
规约侧重于抽象描述系统的核心协议和正确性属性, 通常用于验证分布式协议设计的正确性, 而低层次规约更贴
近实现, 关注具体代码层面的特定逻辑和实现方式, 以支持一致性检查和代码级验证.
(1) 高层次规约
在分布式系统的设计阶段, 关键协议的正确性验证至关重要. 高层次规约用形式化方式精确描述核心协议逻
辑和正确性属性, 避免非正式文档的模糊性和歧义, 同时省略非核心模块和无关细节, 保持高可读性和简洁性. 这
类规约通常在开发初期用于验证设计意图, 发现潜在问题, 并为后续实现提供无歧义的“超级文档”.
共识协议的验证实践: Paxos 和 Raft 等重要分布式协议采用了模型检验验证设计的正确性. Paxos 由
[8]
[9]
Lamport [36] 提出, 并使用 TLA+ 进行验证, 这种方式比手写数学验证可靠 [117] , 比定理证明轻量, 后续许多共识协议
的设计 (如 Raft) 也沿用了这一方式 [37,118] . MongoDB 使用 TLA+ 验证其基于拉取的 Raft 变体 [24] , 阿里巴巴
PolarDB [119] 、腾讯 PaxosStore [120] 、Kafka [121] 、TiKV [25] 、Microsoft CCF (confidential consortium framework) [122] 等系
[5]
统亦采用 TLA+ 进行验证其改进后的核心协议. 开源项目如 etcd 和 ZooKeeper [6,10] , 社区也提供了 TLA+ 规约以
检验其实现和改进的 Raft [123] 和 Zab 协议 [73,124] .
近年来, 越来越多的工业界公司开始在工业级系统的开发与验证中引入模型检验方法, 并取得了显著成效. 本
文梳理了若干具有代表性的实践案例如下.
● Amazon. 2014 年, AWS 团队分享了 TLA+ 在复杂系统设计中的成功经验 [22] . 他们发现, TLA+ 规约 (通常仅
数百行) 能够发现其他方法难以发现的深层缺陷, 即使未发现缺陷, 也能显著增强信心并得以支持激进优化. TLA+
在 Amazon 内部推广后, 成为复杂系统设计流程的一部分. 此外, AWS 还开发了轻量级形式化方法, 利用 Rust 语
言直接编写模型 [125] , 以提升规约编写效率, 并借此避免了 16 个缺陷进入产品.
● Microsoft. Azure Cosmos DB 采用 TLA+ 建模接口层 [23] , 规约仅 390 行, 却帮助解释了一个持续 28 天的高
优先级故障的根本原因. 然而, 团队仍担忧规约与代码缺乏互动可能导致遗漏缺陷. Microsoft CCF 采用 TLA+发现