Formal Agent Contracts
ドキュメント
マルチエージェント開発に形式手法をもたらすClaude Codeプラグイン。VDM-SLでエージェント間契約を定義し、VDMJで構文・型チェックと証明責務生成を行い、必要に応じてZ3で証明可能なPOを検証し、ランタイム契約エンフォースメント付きのTypeScript/Pythonコードを生成します。v2.0ではPhase 2設計文書（PROTOCOL.md, API-SIGNATURES.md）の生成支援と契約テスト自動生成、v2.2ではモジュール単位のモデルルーティングによるトークン削減を追加。すべてClaudeとの自然言語対話を通じて実現。
何ができるのか？
複数のAIエージェントがシステム構築に協調するとき、入出力と保証についての明確な合意が必要です。自然言語仕様は曖昧すぎ、テストは書いたケースだけをカバーします。このプラグインにより、数学的に正確な契約を定義し、仕様段階の機械的チェック、証明可能な範囲のPO検証、ランタイム契約チェックを組み合わせられます。テスト生成は具体例による確認であり、数学的証明そのものではありません。
定義
自然言語 → VDM-SL
検証
構文・型チェック、PO生成
証明
POの範囲でSMT証明
生成
TypeScript / Pythonコード
設計文書
NEWPROTOCOL.md生成
テスト生成
NEW有限ケースの契約テスト生成
インポート
MD仕様 → VDM-SL変換
エクスポート
VDM-SL → 自然言語仕様書
保証範囲の整理
VDM-SLを使うこと自体は「証明」を意味しません。各ステップは保証範囲が異なります。
形式仕様を書く
VDM-SLで型・pre/post・invを明示する。まだ証明ではありません。
仕様をチェックする
VDMJで構文・型チェックとPO生成を行う。PO生成は証明の入口です。
証明する
Z3等でPOを証明する。証明対象として定式化された性質の範囲に限られます。
テストする
仕様や生成コードを具体例で実行確認する。有限ケースの確認であり証明ではありません。
形式手法の専門知識は不要です。Claudeがすべてのステップをガイドし、結果を平易な言語で説明します。
テストは「書く」から「導出する」へ
仕様を厳密に定めることの、最も大きな見返りのひとつはテストです。不変条件・事前条件・事後条件・遷移規則は、それ自体が「何が正しいか」の判定器（テストオラクル）になります。テストケースを人が一つずつ書き起こす必要がなくなり、仕様から機械的に導き出せるようになります。
境界値も遷移も、仕様から列挙
「タイトルは100文字以内」と書けば100文字/101文字の境界値テストが、状態遷移規則を書けば全遷移パターンのテストが、generate-testsスキルで機械的に列挙されます。
生成量は事実上無尽蔵
VDM-SLには組合せテスト（traces）という標準機能があり、操作列のテンプレートから数十万〜数百万規模のテスト列をVDMJが機械展開し、縮約して実行できます。QuickCheckによる証明責務のランダム探索も同様です。テスト量の上限が「人の労力」から「計算資源」に変わる、と言っても差し支えありません。
仕様変更に追従して再導出
テストは仕様という単一ソースから導出されるため、仕様を変えたら再生成するだけです。手書きテスト資産に起きがちな陳腐化やドリフトが、構造的に起きません。
ただし、どれだけ大量に生成しても、有限のテスト実行は証明ではありません（上の「保証範囲の整理」参照）。だからこそ本プラグインは、テスト生成とPO検証・Z3による証明を併用する設計になっています。
最近の新機能（v2.0〜v2.2）
Phase 2 設計文書の生成支援
VDM-SL仕様（Phase 1）から詳細設計（Phase 2）へのブリッジを改良。PROTOCOL.mdでメッセージ型名をSingle Source of Truthとして管理し、API-SIGNATURES.mdで共有モジュールの関数シグネチャを規定。AI駆動開発で頻発する「メッセージ型名の不一致」「フィールド名の揺れ」を、詳細設計フェーズの充実により構造的に防止。verify-specによる設計文書の完全性チェックにも対応。
契約テスト自動生成
VDM-SL仕様（型不変条件・事前条件・事後条件）と設計文書（PROTOCOL.md・API-SIGNATURES.md）の両方からJest/Vitest互換の契約テストを自動生成。型バリデーション、境界値、プロトコル準拠、状態遷移の各テストをカバーし、仕様・設計・実装の乖離を実行時に検出します。
DBスキーマ導出（v2.1.0）
VDM-SLの型・不変条件から、番号付きの写像規則（R1〜R18）でDBスキーマ（DDL）を導出。record型はテーブルに、不変条件はCHECK/UNIQUE/FK/トリガー制約になります。DDLで表現しきれない箇所（nat→BIGINT、遷移規則、複数行にまたがる不変条件）は DEVIATIONS（retrenchment表）に具体的な補償手段とともに記録し、TRACEABILITY 対照表が各不変条件を担保箇所に対応付けます。
モデルルーティング（v2.2.0）
契約に含まれる客観的な複雑度シグナル（陰仕様の数・不変条件・限量子・PO件数）から、モジュールごとに最適なモデル層（light / standard / heavy）を割り振り、コード生成・テスト生成フェーズのトークン消費を抑えます。検証ゲートは不変のまま — どのモデルが生成しても同じVDMJチェックと契約テストが判定し、検証に2回失敗したモジュールは自動で1層エスカレーションします。
開発背景
マルチコンポーネント構成のシステムをAI駆動で開発する際、詳細設計フェーズ（Phase 2）を省略してVDM-SL仕様から直接コード生成すると、メッセージ型名の不一致などの統合バグが発生しがちです。これはVDM-SLの限界ではなく、VDM-SL仕様→詳細設計→実装というフローにおけるPhase 2の欠如が原因でした。v2.0ではこのギャップを埋めます。
ドキュメント
はじめに
ここから始める5分未満でインストール、前提条件、最初の契約実装まで進めます。
スキルリファレンス
リファレンス全15スキルの完全リファレンス: フォワード8スキル（define-contract、verify-spec、smt-verify、generate-code、generate-tests、generate-db-schema、route-models、integrated-workflow）＋ リバース4スキル（extract-spec、refine-spec、reconcile-code、reverse-workflow）＋ 入出力2スキル（import-natural-spec、export-human-spec）＋ リファレンス1スキル（formal-methods-guide）。
例とチュートリアル
チュートリアルTask Managerの例を段階的に紹介します。自然言語からVDMJでチェックされた仕様、実行可能なTypeScriptコードまで。
設定とAPI
上級ランタイム契約トグル、VDMJ設定、Z3統合、VDM-SL型マッピング表、環境変数。
評価レポート
NEWプラグイン使用群と非使用群の定量比較実験結果。3課題×各群5試行・計30試行の探索的な結果として、仕様カバレッジやテスト有効性へのプラスの効果が示唆されています。
クイックインストール
/plugin marketplace add anthropics/claude-plugins-community /plugin install formal-agent-contracts@claude-community
Claude公式のコミュニティディレクトリに掲載されているため、/plugin メニューの Discover からも見つけられます。その後、「新しいエージェントの完全ワークフローを実行して」と指示すれば、Claudeがパイプライン全体をガイドします。
最新版をすぐ試したい場合は、リポジトリを直接追加することもできます（公式ディレクトリは反映に時間差がある場合があります）：
/plugin marketplace add kotaroyamame/formal-agent-contracts /plugin install formal-agent-contracts@formal-agent-contracts