用途：该技能按 Leslie Lamport 的风格指导分布式系统设计。Lamport 是逻辑时钟、Paxos 共识算法、TLA+ 规范语言与 LaTeX 的发明者，其工作构成现代分布式系统的理论基础。核心观点是分布式系统过于复杂，无法靠非形式化推理说清，形式化规范不是可选项而是必需。
主要能力与设计原则：形式化规范优先，先写规范再写代码；时间是逻辑的而非物理的，使用 happens-before 而非墙上时钟；安全属性优先于活性属性，先确保坏事不发生，再确保好事最终发生；用状态机构模系统。写代码时应始终形式化规范、显式定义安全与活性属性、用逻辑时间戳排序事件、把故障建模进规范、实现前证明正确性、考虑所有交错；绝不假设网络可靠、不依赖同步时钟、不忽略故障模式、不靠测试“测出正确性”、不空谈“最终一致性”。
提供的代码模式：Lamport 逻辑时钟（tick/send/receive，接收取 max 后加一）、向量时钟（逐元素取 max 再自增，可比较 before/after/equal/concurrent）、TLA+ 的 SimpleConsensus 模块（类型不变式、Agreement、Validity、Termination、Init/Propose/Decide/Next/Spec）、简化单法令 Paxos（prepare/accept 两阶段与多数派判断）、状态机复制（若所有副本从同一状态出发并按同一顺序应用同一操作，则终态相同）。资料还给出心智模型与标志性动作。
适用场景与限制：适用于分布式协议、共识算法的设计与正确性推理。资料未提供安装方式、运行命令、许可证、价格或平台支持信息，暂未提供。