Formal Agent Contracts
バージョン 2.2.0 ｜ マルチエージェント開発における形式手法ツールキット。エージェント間の契約をVDM-SLで定義し、自動検証する。
形式手法の知識がない開発者でも、Claudeの支援により：
- エージェント間のインターフェースを厳密に定義できる（VDM-SL）
- Phase 2設計文書（PROTOCOL.md、API-SIGNATURES.md）を生成し、仕様と実装の距離を縮められる
- VDMJによる構文チェック・型チェック・証明責務（PO）生成を実行できる
- POから翻訳したSMT命題をZ3で確認し、反例候補を探索できる（元POとの意味の対応・実装適合は別途確認）
- 仕様の型・不変条件からDBスキーマ（DDL）を導出し、乖離（DEVIATIONS）と担保箇所（TRACEABILITY）を記録できる
- 仕様からTypeScript/Pythonのコードスキャフォールドと契約テストを自動生成できる
- 既存コードから仕様を逆抽出し、対話で磨き上げ、コードと照合できる（リバースワークフロー）
- モジュールごとに「能力が足りる範囲で最も軽いモデル」を割り振り、生成フェーズのトークン消費を抑えられる（契約駆動モデルルーティング、v2.2.0）
確認できる範囲
仕様記述、VDMJによる構文・型検査とPO生成、翻訳したSMT命題の結果、実装の有限テストを分けて報告します。PO生成は証明ではなく、SMTの unsat は翻訳や生成実装の正しさまで証明しません。未実行・未対応・unknown・timeout・実行エラーを合格に含めません。結果には入力・ツール・コマンド・ログ・仮定・未確認範囲を残します。
TaskManager基準例 は配布実装を直接テストします。再現手順と意味の差分を確認してください。
インストール
Claude Code のプラグインとしてインストール：
/plugin marketplace add kotaroyamame/formal-agent-contracts
/plugin install formal-agent-contracts@formal-agent-contracts
コミュニティマーケットプレース経由でもインストールできます：
/plugin marketplace add anthropics/claude-plugins-community
/plugin install formal-agent-contracts@claude-community
コミュニティカタログは特定コミットに固定されて夜間同期で追従するため、最新版（v2.1 以降の DBスキーマ導出・モデルルーティングなど）が入っていない場合はリポジトリのマーケットプレースを使ってください。
スキル一覧（全15スキル）
フォワード開発（仕様 → コード）
| スキル | 説明 |
|---|
| define-contract | 自然言語での対話からVDM-SL契約と設計文書（PROTOCOL.md、API-SIGNATURES.md）を段階的に生成 |
| verify-spec | VDMJによる構文チェック・型チェック・PO生成。設計文書の完全性チェックとVDM-SL仕様との一貫性確認も実行 |
| smt-verify | POをSMT-LIBに翻訳し、Z3で命題の充足性を確認（反例候補の探索） |
| generate-db-schema | VDM-SLの型・不変条件からDBスキーマ（DDL）を規則的に導出。表現しきれない乖離は DEVIATIONS（retrenchment表）、担保箇所は TRACEABILITY に記録 |
| generate-code | VDM-SL仕様からTypeScript/Pythonのコードスキャフォールドを生成（事前条件・事後条件・不変式のランタイム検証コード付き） |
| generate-tests | VDM-SL仕様と設計文書からJest/Vitest互換の契約テストを自動生成（型不変式・契約遵守・状態遷移・境界値） |
| integrated-workflow | 定義→検証→SMT確認→コード生成→テストの5フェーズを一気通貫で実行 |
| route-models | 契約の客観的な複雑度シグナル（暗黙的定義・不変条件・PO件数など）からモジュールごとに能力が足りる範囲で最も軽いモデル層（light/standard/heavy）を割り振り、生成フェーズのトークン消費を削減。検証ゲートは不変で、同一モジュールで2回検証に失敗した場合のみ自動で1層エスカレーション |
リバース開発（既存コード → 仕様）
| スキル | 説明 |
|---|
| extract-spec | 既存コードから暫定VDM-SL仕様を抽出（対話の足場となる仮仕様） |
| refine-spec | 対話を通じて仮仕様を磨き、ユーザーの頭の中にある「真の仕様」を引き出す |
| reconcile-code | 確定した仕様と既存コードを項目ごとに照合し、差分レポート・修正・テストを生成 |
| reverse-workflow | 抽出→洗練→照合のリバースパイプラインを一気通貫で実行（フォワードパイプラインへの接続も可能） |
仕様の入出力
| スキル | 説明 |
|---|
| import-natural-spec | 自然言語の仕様書（Markdown）を読み込み、曖昧さを対話で解消しながらVDM-SL仕様へ変換 |
| export-human-spec | VDM-SL仕様から非エンジニアも読める自然言語仕様書（Markdown）を生成 |
リファレンス
| スキル | 説明 |
|---|
| formal-methods-guide | VDM-SLの文法、型システム、PO種別などの背景知識を提供（他スキルからも参照される） |
セットアップ（外部ツール）
スキルによって必要な外部ツールが異なります。使うスキルに応じてインストールしてください。
define-contract、formal-methods-guide、import-natural-spec、export-human-spec などの対話系スキルは外部ツールなしで動作します。
使い方
最初のプロンプトの雛形は prompt-templates.md を参照してください。単一エージェント定義、マルチエージェント境界契約、統合ワークフロー、既存仕様の形式化、リバースワークフロー、検証・自動証明、契約テスト生成の7テンプレートがあります。
最小の例：
在庫管理エージェントを定義して。
- 商品には商品ID・商品名・在庫数がある
- 在庫数は0未満にならない
- 出荷数は現在の在庫数を超えられない
→ define-contract が対話的に契約を深掘りし、VDM-SL仕様を生成します。その後「検証して」でverify-spec、「テストを生成して」でgenerate-testsへ続きます。
リポジトリ構成
| パス | 内容 |
|---|
skills/ | 15スキルの定義（各スキルは SKILL.md、多くは references/ 付き） |
examples/ | 動作例（task-manager: VDM-SL仕様 → TypeScript実装 → SMT-LIB確認） |
eval/ | 評価フレームワーク（ベンチマーク課題、実行ログ、採点スクリプト、結果） |
design/ | 設計文書（reverse-workflow-design.md — リバースワークフローの設計時ドキュメント） |
prompt-templates.md | ユーザー向けプロンプトテンプレート集 |
評価
過去の30成果物と集計を履歴として保存しています。対照群には意図的な欠落の記録があり、旧集計はヒューリスティック採点を含むため、通常開発に対する効果の比較証拠としては扱いません。旧mutation runnerには起動失敗やタイムアウトをkillに数える問題もあり、過去の100%という値を検出性能の根拠には使いません。成果物は欠陥検出用fixtureとして活用します。
修正した評価器の再現手順・判定状態は eval/README.md、過去の数値と限界は eval/results/report.md を参照してください。
変更履歴
CHANGELOG.md を参照してください。
今後の予定
作者
IID Systems (https://iid.systems)
ライセンス
MIT — LICENSE を参照
