マルチエージェント開発に「数学的な契約」を導入する ── Formal Agent Contracts プラグインの使い方

マルチエージェント開発、境界で壊れる問題

複数のAIエージェントが協調してシステムを構築する時代が来ています。しかし、エージェントの数が増えるほど境界で問題が起きます。Agent Aが返すデータの形式をAgent Bが誤って解釈する。テストは各モジュール単体では通るのに、結合した瞬間に壊れる。原因は「仕様が曖昧だった」の一言に集約されます。

自然言語の仕様書は、書いた人と読む人で解釈が異なり得ます。テストは有限個のケースしかカバーできません。では、エージェント間の「約束事」を数学的に厳密に定義し、機械的に検証できたらどうでしょうか。

Formal Agent Contracts は、それを実現するClaude Codeプラグインです。

何ができるのか

このプラグインは6つのスキルで構成されています。

スキル	できること
define-contract	自然言語でエージェントの役割を説明 → VDM-SL形式仕様に変換
verify-spec	VDMJで構文チェック・型チェック・証明責務（PO）の自動生成
smt-verify	POをSMT-LIBに変換し、Z3ソルバーで自動証明
generate-code	仕様からTypeScript/Pythonのスキャフォールドを生成（ランタイム契約チェック付き）
integrated-workflow	定義→検証→証明→生成→テストを1セッションで一気通貫実行
formal-methods-guide	VDM-SLの文法や概念をClaudeが解説

重要なポイント：VDM-SLの知識は不要です。Claudeが自然言語から形式仕様への変換を担当するので、開発者はドメイン知識に集中できます。

セットアップ

前提ソフトウェア

Java 11以上（VDMJの実行に必要）と、SMT証明を使う場合はPython 3.8以上が必要です。

# VDMJ のインストール（仕様検証エンジン）
mkdir -p ~/.vdmj
curl -L -o ~/.vdmj/vdmj.jar \
  https://github.com/nickbattle/vdmj/releases/latest/download/vdmj-4.6.0-SNAPSHOT.jar

# Z3 のインストール（SMT自動証明、任意）
pip install z3-solver

プラグインのインストール

Claude Codeのセッション内で以下を実行します。

/plugin install formal-agent-contracts@iid

これだけで6つのスキルが使えるようになります。

実践：タスク管理エージェントを作る

抽象的な説明より、手を動かしたほうが早いです。タスク管理エージェントを題材に、プラグインの全ステップを体験してみましょう。

Step 1: 契約を定義する

Claudeに自然言語で伝えるだけです。

あなた: タスク管理エージェントを定義して。
        タスクにはID・タイトル・ステータス（Todo/InProgress/Done）・
        優先度（Low/Medium/High）がある。
        Doneになったタスクは他のステータスに戻せないようにしたい。

Claudeが define-contract スキルを起動し、VDM-SL仕様を生成します。

types
  Status = <Todo> | <InProgress> | <Done>;
  Task :: id     : nat1
          title  : seq1 of char
          status : Status
  inv t == len t.title <= 100;

operations
  ChangeStatus: TaskId * Status ==> ()
  ChangeStatus(taskId, newStatus) == ...
    pre  taskId in set dom board and
         ValidTransition(board(taskId).status, newStatus)
    post board(taskId).status = newStatus;

ここで登場する3つの概念が「契約」の核心です。

• pre（事前条件） ── この操作を呼ぶ前に満たすべき条件。「タスクが存在し、遷移が有効であること」
• post（事後条件） ── 操作の実行後に保証される状態。「ステータスが確かに更新されていること」
• inv（不変条件） ── 常に成り立つルール。「タイトルは100文字以内」

これらが数学的に厳密な「エージェント間の約束事」になります。

Step 2: 仕様を検証する

あなた: この仕様を検証して

Claudeが裏でVDMJ（VDM-SLの参照実装ツール）を実行し、結果を分かりやすく報告します。

✅ 構文チェック: PASSED
✅ 型チェック: PASSED
📋 証明責務（PO）: 38件生成
   - CreateTask実行後、TaskBoard不変条件を満たすか
   - ChangeStatus実行後、タイトルが変わっていないか
   - DeleteTask実行後、ボードのサイズが正確に1減るか

証明責務（Proof Obligation） は、仕様の pre/post/inv から自動的に導出される「この契約は本当に守れるか？」という検証項目です。自分で考える必要はありません。

Step 3: Z3で自動証明する

あなた: POをZ3で証明して

ClaudeがPOをSMT-LIB形式に変換し、Z3ソルバーで解きます。

PO #12 (ChangeStatusがタイトルを保存): ✅ 証明済み
PO #15 (DeleteTaskのカーディナリティ): ✅ 証明済み
PO #23 (CreateTaskの不変条件):         ✅ 証明済み
...
37/38 証明済み、1件 unknown（手動レビュー推奨）

Step 4: コードを生成する

あなた: TypeScriptでコードを生成して

VDM-SL仕様からランタイム契約チェック付きのTypeScriptコードが生成されます。

changeStatus(taskId: TaskId, newStatus: Status): void {
  // --- 事前条件（VDM-SL仕様から） ---
  checkPre(
    this.board.has(taskId),
    `taskId ${taskId} not in dom board`
  );
  checkPre(
    validTransition(this.board.get(taskId)!.status, newStatus),
    `Invalid transition: ${this.board.get(taskId)!.status} → ${newStatus}`
  );

  // --- 操作本体 ---
  const task = this.board.get(taskId)!;
  const updated = { ...task, status: newStatus };
  this.board.set(taskId, updated);

  // --- 事後条件（VDM-SL仕様から） ---
  checkPost(
    this.board.get(taskId)!.status === newStatus,
    `status must be ${newStatus}`
  );
}

契約違反を試してみます。

agent.changeStatus(taskId, "Todo");
// → ContractError: Pre-condition failed:
//   Invalid transition: Done → Todo

サイレントなバグではなく、何がどう違反したかが即座に分かります。

一気通貫モード

個別ステップを踏まなくても、1コマンドで全パイプラインを実行できます。

あなた: 統合ワークフローでタスク管理エージェントを開発して

Claudeが 定義→検証→証明→生成→テスト を自動で実行し、最後にセッションレポートを出力します。途中でエラーが出れば自動的に前のフェーズに戻って修正します。

なぜテストではなく「契約」なのか

テストは帰納的です。有限個のケースを確認して「たぶん大丈夫」と判断します。100個のテストをパスしても、101番目のケースで壊れるかもしれません。

形式的契約は演繹的です。「すべての入力に対してこの性質が成り立つ」ことを数学的に証明します。

具体例で見てみます。

// 契約なし：静かに成功する。バグは後で別の場所で発覚する
task.status = "Todo";  // Doneだった。本来は禁止すべき遷移！

// 契約あり：即座に明確なエラー
changeStatus(taskId, "Todo");
// → ContractError: Invalid transition: Done → Todo

さらに、仕様はそのまま生きたドキュメントになります。各エージェントが何をするか、何を期待するか、何を保証するかが厳密に記述されており、コードと乖離することがありません（コードが仕様から生成されるため）。

まとめ

観点	従来のアプローチ	Formal Agent Contracts
仕様の記述	自然言語（曖昧）	VDM-SL（数学的に一意）
正しさの確認	テスト（有限ケース）	形式的証明（全ケース）
バグの検出タイミング	実行時・結合時	仕様定義時・証明時
エージェント間の合意	暗黙的	機械検証可能な契約

形式手法は難しいものだと思われがちですが、このプラグインではClaudeが形式仕様の読み書きを担当します。開発者は「何をしたいか」を自然言語で伝えるだけです。

リンク

• プラグインのインストール: Claude Codeで /plugin install formal-agent-contracts@iid
• ソースコード: github.com/kotaroyamame/formal-agent-contracts
• 動作例（タスク管理）: プラグイン内 examples/task-manager/
• 研究論文: Formal-Spec-Driven Development
• IID Systems: iid.systems