用途：编写非平凡 TLA+ 规约，运行 TLC 模型检查器，并在形式化规约与实现代码之间建立对应关系。适用对象包括建模分布式系统、协议、并发算法和状态机的开发者。
主要能力：提供语言与 PlusCal 语法参考，分布式系统、协议、不变量等模式参考，以及基础、PlusCal 和分布式系统三类模板；提供完整检查、仅解析、PlusCal 转 TLA+、TLC 模型检查等脚本，也支持直接调用 Java 工具进行解析、翻译、模型检查和 REPL；支持导出状态图用于可视化。
使用方式：首次运行 bash SKILL_DIR/scripts/setup.sh 下载 tla2tools.jar（v1.8.0）并检查 Java 11+。完整检查用 bash SKILL_DIR/scripts/check.sh spec.tla --config spec.cfg；仅解析用 bash SKILL_DIR/scripts/parse.sh spec.tla；PlusCal 转译用 bash SKILL_DIR/scripts/translate.sh spec.tla -nocfg；模型检查用 bash SKILL_DIR/scripts/tlc.sh spec.tla --config spec.cfg --workers auto。也可直接执行 java -cp "$JAR" tlc2.TLC -workers auto -config spec.cfg spec.tla。每个规约需要配套 .cfg 文件配置常量、不变量、性质、约束和死锁检查。
适用场景与限制：适合并发与分布式系统的建模、缺陷查找、规约与代码一致性分析。建议从小常量开始，先加类型不变量，再逐条添加安全性性质，最后考虑带公平性的活性性质。小常量更容易穷尽状态；活性检查通常更慢。默认不假设公平性，需要显式添加 WF_vars 或 SF_vars。TLA+ 中序列从 1 开始索引，每个动作必须为所有变量指定取值，未修改的变量用 UNCHANGED。具体平台支持、收费情况、价格和效果资料暂未提供。