{
  "markdown": "# Formal Agent Contracts\n\n**バージョン 2.2.0** ｜ マルチエージェント開発における形式手法ツールキット。エージェント間の契約をVDM-SLで定義し、自動検証する。\n\n形式手法の知識がない開発者でも、Claudeの支援により：\n\n- エージェント間のインターフェースを厳密に定義できる（VDM-SL）\n- Phase 2設計文書（PROTOCOL.md、API-SIGNATURES.md）を生成し、仕様と実装の距離を縮められる\n- VDMJによる構文チェック・型チェック・証明責務（PO）生成を実行できる\n- Z3によるPOの自動証明・反例探索ができる\n- 仕様の型・不変条件からDBスキーマ（DDL）を導出し、乖離（DEVIATIONS）と担保箇所（TRACEABILITY）を記録できる\n- 仕様からTypeScript/Pythonのコードスキャフォールドと契約テストを自動生成できる\n- 既存コードから仕様を逆抽出し、対話で磨き上げ、コードと照合できる（リバースワークフロー）\n- モジュールごとに「能力が足りる範囲で最も軽いモデル」を割り振り、生成フェーズのトークン消費を抑えられる（契約駆動モデルルーティング、v2.2.0）\n\n## インストール\n\nClaude Code のプラグインとしてインストール：\n\n```\n/plugin marketplace add kotaroyamame/formal-agent-contracts\n/plugin install formal-agent-contracts@formal-agent-contracts\n```\n\n## スキル一覧（全15スキル）\n\n### フォワード開発（仕様 → コード）\n\n| スキル | 説明 |\n|---|---|\n| **define-contract** | 自然言語での対話からVDM-SL契約と設計文書（PROTOCOL.md、API-SIGNATURES.md）を段階的に生成 |\n| **verify-spec** | VDMJによる構文チェック・型チェック・PO生成。設計文書の完全性チェックとVDM-SL仕様との一貫性確認も実行 |\n| **smt-verify** | POをSMT-LIBに変換し、Z3で自動証明・反例探索 |\n| **generate-db-schema** | VDM-SLの型・不変条件からDBスキーマ（DDL）を規則的に導出。表現しきれない乖離は DEVIATIONS（retrenchment表）、担保箇所は TRACEABILITY に記録 |\n| **generate-code** | VDM-SL仕様からTypeScript/Pythonのコードスキャフォールドを生成（事前条件・事後条件・不変式のランタイム検証コード付き） |\n| **generate-tests** | VDM-SL仕様と設計文書からJest/Vitest互換の契約テストを自動生成（型不変式・契約遵守・状態遷移・境界値） |\n| **integrated-workflow** | 定義→検証→証明→コード生成→テストの5フェーズを一気通貫で実行 |\n| **route-models** | 契約の客観的な複雑度シグナル（暗黙的定義・不変条件・PO件数など）からモジュールごとに能力が足りる範囲で最も軽いモデル層（light/standard/heavy）を割り振り、生成フェーズのトークン消費を削減。検証ゲートは不変で、同一モジュールで2回検証に失敗した場合のみ自動で1層エスカレーション |\n\n### リバース開発（既存コード → 仕様）\n\n| スキル | 説明 |\n|---|---|\n| **extract-spec** | 既存コードから暫定VDM-SL仕様を抽出（対話の足場となる仮仕様） |\n| **refine-spec** | 対話を通じて仮仕様を磨き、ユーザーの頭の中にある「真の仕様」を引き出す |\n| **reconcile-code** | 確定した仕様と既存コードを項目ごとに照合し、差分レポート・修正・テストを生成 |\n| **reverse-workflow** | 抽出→洗練→照合のリバースパイプラインを一気通貫で実行（フォワードパイプラインへの接続も可能） |\n\n### 仕様の入出力\n\n| スキル | 説明 |\n|---|---|\n| **import-natural-spec** | 自然言語の仕様書（Markdown）を読み込み、曖昧さを対話で解消しながらVDM-SL仕様へ変換 |\n| **export-human-spec** | VDM-SL仕様から非エンジニアも読める自然言語仕様書（Markdown）を生成 |\n\n### リファレンス\n\n| スキル | 説明 |\n|---|---|\n| **formal-methods-guide** | VDM-SLの文法、型システム、PO種別などの背景知識を提供（他スキルからも参照される） |\n\n## セットアップ（外部ツール）\n\nスキルによって必要な外部ツールが異なります。使うスキルに応じてインストールしてください。\n\n| ツール | 必要とするスキル | 入手先 |\n|---|---|---|\n| Java 11以上 | verify-spec、smt-verify（VDMJの実行に必要） | https://adoptium.net/ |\n| VDMJ | verify-spec、smt-verify | https://github.com/nickbattle/vdmj/releases （`vdmj-suite-*-distribution.zip`）。詳細は [vdmj-setup.md](skills/verify-spec/references/vdmj-setup.md) |\n| Z3 | smt-verify | `pip install z3-solver` または https://github.com/Z3Prover/z3 |\n| Node.js + Vitest/Jest | generate-tests（生成テストの実行） | https://nodejs.org/ |\n| sqlite3 または PostgreSQL | generate-db-schema（任意。生成DDLの実行検証用） | macOS は sqlite3 同梱 / https://www.postgresql.org/ |\n\ndefine-contract、formal-methods-guide、import-natural-spec、export-human-spec などの対話系スキルは外部ツールなしで動作します。\n\n## 使い方\n\n最初のプロンプトの雛形は [prompt-templates.md](prompt-templates.md) を参照してください。単一エージェント定義、マルチエージェント境界契約、統合ワークフロー、既存仕様の形式化、リバースワークフロー、検証・自動証明、契約テスト生成の7テンプレートがあります。\n\n最小の例：\n\n```\n在庫管理エージェントを定義して。\n- 商品には商品ID・商品名・在庫数がある\n- 在庫数は0未満にならない\n- 出荷数は現在の在庫数を超えられない\n```\n\n→ define-contract が対話的に契約を深掘りし、VDM-SL仕様を生成します。その後「検証して」でverify-spec、「テストを生成して」でgenerate-testsへ続きます。\n\n## リポジトリ構成\n\n| パス | 内容 |\n|------|------|\n| `skills/` | 15スキルの定義（各スキルは SKILL.md、多くは references/ 付き） |\n| `examples/` | 動作例（`task-manager`: VDM-SL仕様 → TypeScript実装 → SMT-LIB証明） |\n| `eval/` | 評価フレームワーク（ベンチマーク課題、実行ログ、採点スクリプト、結果） |\n| `design/` | 設計文書（`reverse-workflow-design.md` — リバースワークフローの設計時ドキュメント） |\n| `prompt-templates.md` | ユーザー向けプロンプトテンプレート集 |\n\n## 評価\n\n本プラグインの有無で同一課題（3課題 × 5試行 × 2条件）の成果物を比較した探索的評価を同梱しています。仕様カバレッジ・テスト有効性などで効果を示唆する結果が得られていますが、単一モデルによる生成・ヒューリスティック採点などの方法論的制約があります。結果と限界の詳細は [eval/results/report.md](eval/results/report.md) を参照してください。\n\n## 変更履歴\n\n- **v2.2.0** — 契約駆動モデルルーティング（route-models）：契約の客観的な複雑度シグナルからモジュールごとに能力が足りる範囲で最も軽いモデル層（light/standard/heavy）を割り振り、生成フェーズのトークン消費を削減。検証ゲートは不変で、同一モジュールで2回検証に失敗した場合のみ自動で1層エスカレーション\n- **v2.1.0** — DBスキーマ導出（generate-db-schema）：型・不変条件→DDLの規則的写像（R1〜R18）、retrenchment に基づく乖離記録（DEVIATIONS）、不変条件の担保箇所対照表（TRACEABILITY）\n- **v2.0.0** — Phase 2設計文書（PROTOCOL.md、API-SIGNATURES.md）生成支援、契約テスト自動生成（generate-tests）、設計文書の完全性チェック（verify-spec拡張）\n- **v1.5.0** — import-natural-spec / export-human-spec（自然言語仕様の入出力）\n- **v1.1.0–v1.4.0** — リバースワークフロー（extract-spec、refine-spec、reconcile-code、reverse-workflow）、評価フレームワーク\n- **v1.0.0** — 統合ワークフロー（integrated-workflow）、ドキュメントの日英対応\n- **v0.3.0** — コードスキャフォールド生成（generate-code、TypeScript/Python）\n- **v0.2.0** — SMT-LIB変換とZ3証明（smt-verify）\n- **v0.1.0** — 初版（define-contract、verify-spec、formal-methods-guide）\n\n## 今後の予定\n\n- [ ] design-system スキル（ARCHITECTURE.md / TECH-STACK.md / ADR / 制約ファイルによる技術選定支援）\n- [ ] UI契約とE2Eテスト生成（define-ui-contract / generate-e2e — VDM-SL traces から Playwright テストを導出）\n- [ ] 評価の再実施（独立した採点者・複数モデルでの追試、変異数を増やしたミューテーションテスト）\n- [ ] 実プロジェクトでの適用事例の収集\n\n## 作者\n\nIID Systems (https://iid.systems)\n\n## ライセンス\n\nMIT — [LICENSE](LICENSE) を参照\n",
  "bytes": 4927,
  "sha": "6399ce9038d7eecd8d8b6bff75e4bbf602e52cca9ad96ae4a156e17ea3805473",
  "repo_slug": "kotaroyamame/formal-agent-contracts",
  "fonte": "repo",
  "truncated": false,
  "api": "https://agentalog.com/api/listings/plg_kotaroyamame_formal_agent_contracts_form_065670f0/readme"
}