用途
本技能围绕 Leslie Lamport 的严谨方法，帮助设计分布式系统。Lamport 将分布式系统从临时性工程转变为严谨科学，其逻辑时钟、共识（Paxos）与形式化规格（TLA+）方面的工作，是当今几乎所有可靠分布式系统的理论基础，他于 2013 年获得图灵奖。
核心哲学
资料引用 Lamport 的观点：分布式系统是“一台你甚至不知道其存在的计算机发生故障，就能让你自己的计算机无法使用”的系统；“如果你不写下来就思考，你只是以为自己在思考”；“成为好程序员的方法是写程序，而非学语言”。
设计原则
- 形式化规格优先：写代码前先写精确规格；若无法精确描述，说明尚未理解。
- 时间是相对的：分布式系统中没有全局时钟，应使用逻辑时间（happens-before）推理顺序。
- 状态机复制：任何确定性服务都可通过在多个服务器上复制为状态机来实现容错。
- 安全性与活性：将“必须始终为真”（safety）与“最终必须发生”（liveness）分开，并证明两者。
- 以严谨求简单：最清晰的系统来自精确思考，形式化不是负担而是通往简单的路径。
设计系统时的准则
始终：先写规格（TLA+、Alloy 或精确文字）；定义安全属性（绝不能发生什么）；定义活性属性（最终必须发生什么）；推理并发操作的所有可能交错；物理时间不可靠时使用逻辑时间戳；让系统状态显式、转换清晰；记录所有状态下必须成立的不变量。 绝不要：假设消息有序到达（除非已证明）；假设时钟同步（它们并不同步）；假设故障相互独立（它们常相关）；含糊地说“最终”而不定义什么保证它；对并发系统凭直觉——要么证明，要么穷尽测试；混淆规格与实现。 优先选择：状态机而非临时事件处理；逻辑时钟而非物理时间戳排序；关键状态用共识协议而非乐观并发；显式故障处理而非隐式假设；已证明的算法而非聪明的启发式。
关键概念
逻辑时钟（Lamport 时间戳）：每个进程维护计数器 C；任何事件前自增 C；发送消息时带上 C；收到时间戳为 T 的消息时设 C = max(C, T) + 1。这给出偏序：若 a → b，则 C(a) < C(b)，但 C(a) < C(b) 不蕴含 a → b。 Happens-Before 关系（→）：满足以下之一时 a → b：a 与 b 在同一进程且 a 在前；或 a 是发送、b 是对应接收；或存在 c 使 a → c 且 c → b（传递性）。若 a → b 与 b → a 均不成立，则两事件并发。 状态机复制：将服务建模为确定性状态机；跨 N 个服务器复制；用共识（Paxos/Raft）就输入序列达成一致；每个副本按相同顺序应用输入，得到相同状态。2F+1 个副本可容忍 F 个故障。 Paxos（简化）：三种角色 Proposer、Acceptor、Learner。阶段一（Prepare）：Proposer 向 acceptors 发送 PREPARE(n)；acceptor 返回其已接受的编号最高的提案（若有）。阶段二（Accept）：若 proposer 收到多数响应，发送 ACCEPT(n, v)，其中 v 是所见编号最高的值（或新值）；acceptor 若未承诺更高编号提案则接受。多数接受同一 (n, v) 即达成共识。
思维模型与 TLA+ 方法
以数学家的方式处理分布式系统：精确定义问题（输入、输出、允许的行为）；识别不变量（什么必须始终为真）；考虑所有交错（事件任意顺序会发生什么）；证明正确性（安全性与活性成立）；然后实现（代码应是规格的直接翻译）。 TLA+ 方法：定义状态空间；定义初始状态谓词；定义下一状态关系（允许的转换）；将安全性指定为不变量（始终为真）；将活性指定为时序属性（最终为真）；通过模型检查或证明验证规格满足属性。
代码模式
资料给出两个 Python 类示例。LamportClock 包含 tick()（本地事件前自增）、send_timestamp()（获取出站消息时间戳）、receive(msg_timestamp)（接收消息时更新时钟，设 _time = max(_time, msg_timestamp) + 1）。VectorClock 以 node_id 与 num_nodes 初始化时钟字典，提供 tick()、send()（tick 后返回时钟副本）、receive(other)（逐节点取最大值后 tick）以及 happens_before(other)（判断 self → other）。
适用场景与限制
本技能面向需要为并发、容错、共识类系统建立正确性论证与形式化规格的开发者与架构师。资料同时列出“警告信号”：若你未加证明就假设“实践中这永远不会发生”；若分布式算法“大多数时候”能工作；若写不出系统维持的不变量；若在分布式系统中用墙钟时间排序；若未考虑网络分区期间的行为；若系统没有形式化规格——则说明违背了 Lamport 的原则。资料还提到进一步阅读 philosophy.md 与 references.md。以上未在本字段展开的具体收费、平台支持、安装命令等信息，原文暂未提供。