TLA+

概述

TLA+（Temporal Logic of Actions）是 Leslie Lamport 设计的形式化规约语言，用集合论与时序逻辑描述系统的状态与状态转移，配套模型检查器 TLC 可穷举状态空间，自动发现违反不变式或活性性质的执行路径。

用途

它特别适合验证并发与分布式协议中人脑难以枚举的边界情形：死锁、消息乱序、崩溃重启交织等。规约与实现分离，工程师先用 PlusCal（类伪代码前端）或原生 TLA+ 写出算法骨架，再验证性质。

应用

亚马逊 AWS 公开撰文称用 TLA+ 在 S3、DynamoDB 等系统中发现了测试难以触及的深层设计缺陷；微软、MongoDB、TiDB 等也用它验证共识与复制协议。Raft 与 Paxos 的多个变体均有公开的 TLA+ 规约。