mcpField
T
tla-plus-expert

tla-plus-expert

github.com/rysweetテスト・品質7647 回インストール21 週間前に更新
リポジトリ

tla-plus-expert について

tla-plus-expert は、amplihack で TLA+ の形式仕様を扱うスキルです。専門エージェントに委任し、仕様の作成・レビュー、TLC によるモデル検査、PlusCal との変換を支援します。

主な機能

  1. 01TLA+ 仕様の作成とレビュー
  2. 02TLC の設定とトレース解釈
  3. 03不変条件・活性・安全性の検討
  4. 04PlusCal と TLA+ の変換支援
  5. 05amplihack の実験基盤との連携

活用シーン

  1. 01並行・分散プロトコルの仕様化
  2. 02TLA+ 仕様の正しさのレビュー
  3. 03TLC の反例の解釈
  4. 04amplihack コンポーネントへの形式手法の適用

インストール

コマンドをコピーしてターミナルで実行します。

$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 エージェントに処理を委任します。

  1. TLA+ 言語と慣用表現 — 仕様、演算子、時相論理式の作成
  2. TLC モデル検査器 — 設定、トレースの解釈、状態空間の管理
  3. 7 つのメンタルモデル（Demirbas）— 抽象化、グローバル共有メモリ、ローカルガード、不変条件、段階的な詳細化、原子性の詳細化、通信
  4. 業界の事例研究 — AWS、MongoDB、Microsoft Azure における本番環境での 8 つの活用事例
  5. AI と TLA+ の限界 — LLM の能力とガードレールに関する SysMoBench の知見
  6. amplihack の実験インフラストラクチャ — マニフェスト駆動の実験、ヒューリスティックによるスコアリング、TLC 検証の統合

既存インフラストラクチャとの統合

amplihack リポジトリには、次の機能を備えた TLA+ 実験ランナー crates/amplihack-eval/src/tla_prompt_experiment.rs が含まれています。

  • マニフェスト駆動の実験マトリックス（モデル x プロンプトのバリアント x 反復回数）
  • 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 対応