mcpField
T
tla-plus-expert

tla-plus-expert

github.com/rysweet测试与质量7647 次安装21 周前更新
代码仓库

关于 tla-plus-expert

tla-plus-expert 是用于 amplihack 中 TLA+ 形式化规约工作的技能，委派专门 Agent 协助编写和审查规约、使用 TLC 模型检查及转换 PlusCal。

主要功能

  1. 01编写和审查 TLA+ 规约
  2. 02配置 TLC 并解读执行轨迹
  3. 03分析不变式、活性与安全属性
  4. 04协助转换 PlusCal 与 TLA+
  5. 05支持 amplihack 实验基础设施

适用场景

  1. 01为并发或分布式协议编写规约
  2. 02检查 TLA+ 规约的正确性
  3. 03理解 TLC 反例
  4. 04在 amplihack 组件中应用形式化方法

安装

复制下面的命令，在终端中运行。

$npx skills add https://github.com/rysweet/amplihack --skill tla-plus-expert

安装后在 Claude Code 中输入/tla-plus-expert确认已加载。

详细介绍

TLA+ 专家技能

目的

在 amplihack 中，为并发和分布式系统的设计、验证与推理提供专家级的 TLA+ 形式化规范辅助。

此技能的触发条件

  • 用户要求编写或审查 TLA+ 规范
  • 用户需要有关模型检查（TLC）配置或输出解读方面的帮助
  • 用户希望对协议或工作流设计进行形式化验证
  • 用户询问不变式、活性属性或安全属性
  • 用户希望将形式化方法应用于 amplihack 组件
  • 用户提到 PlusCal，或希望在 PlusCal 与 TLA+ 之间进行转换
  • 用户提及 Lamport、Demirbas 或形式化方法最佳实践

工作原理

此技能委派给 tla-plus-expert Agent，该 Agent 深入了解：

  1. TLA+ 语言与惯用法——编写规范、运算符和时态公式
  2. TLC 模型检查器——配置、轨迹解读和状态空间管理
  3. 七种思维模型（Demirbas）——抽象、全局共享内存、本地守卫、不变式、逐步细化、原子性细化、通信
  4. 行业案例研究——来自 AWS、MongoDB、Microsoft Azure 的 8 个生产环境应用案例
  5. AI + TLA+ 的局限性——SysMoBench 关于 LLM 能力和防护措施的研究结果
  6. amplihack 实验基础设施——由清单驱动的实验、启发式评分、TLC 验证集成

与现有基础设施的集成

amplihack 仓库包含一个 TLA+ 实验运行器，位于 crates/amplihack-eval/src/tla_prompt_experiment.rs，具备以下功能：

  • 由清单驱动的实验矩阵（模型 × 提示词变体 × 重复次数）
  • 6 个启发式评分维度
  • 支持真实 TLC 验证
  • 回放和实时执行模式

TLA+ 规范位于 experiments/hive_mind/tla_prompt_language/specs/。

使用示例

# Write a spec for a new protocol
/tla-plus-expert Write a TLA+ spec for our consensus voting workflow

# Review an existing spec
/tla-plus-expert Review specs/SmartOrchestrator.tla for correctness

# Help with TLC output
/tla-plus-expert TLC found a counterexample in my spec, help me understand it

# Decide if TLA+ is appropriate
/tla-plus-expert Should I formally specify this retry cascade logic?

# Generate invariants
/tla-plus-expert What invariants should I check for a parallel workstream manager?

关键资源

  • TLA+ 规范：experiments/hive_mind/tla_prompt_language/specs/
  • 实验运行器：crates/amplihack-eval/src/tla_prompt_experiment.rs
  • TLC 二进制文件：/usr/local/bin/tlc（如果已安装）
  • Issue #3939：TLA+ 集成路线图

评论

支持 Markdown