はじめに
5分未満で、VDMJによる構文・型チェックとランタイム契約チェック付きのエージェント実装まで進めます。このガイドではインストール、前提条件、最初のエンドツーエンドワークフローをカバーします。
前提条件
プラグインはClaude Code内で動作します。完全な機能を使うには、以下のツールも必要です:
VDMJ
必須構文チェック、型チェック、証明責務生成用のVDM-SLツールチェーン。
- Java 11以上
- VDMJリリースページからダウンロード VDMJ Releases
- vdmj-suite-*-distribution.zip を展開して vdmj.sh をPATHに追加（または Maven Central の単体jarを ~/.vdmj/vdmj.jar に配置）
Z3ソルバー
オプション証明責務の自動証明用SMTソルバー。smt-verifyスキルを使う場合のみ必要。
pip install z3-solver
Node.js + Vitest/Jest
オプションgenerate-testsスキルが生成する契約テストの実行に必要。
インストール
formal-agent-contracts は Claude 公式のコミュニティディレクトリに掲載されています。/plugin メニューの Discover から、または次のコマンドでインストールできます:
/plugin marketplace add anthropics/claude-plugins-community /plugin install formal-agent-contracts@claude-community
最新版をすぐ試したい場合は、リポジトリを直接マーケットプレースとして追加します（公式ディレクトリは反映に時間差がある場合があります）:
/plugin marketplace add kotaroyamame/formal-agent-contracts /plugin install formal-agent-contracts@formal-agent-contracts
5分で最初の契約を定義
シンプルなエージェント契約を定義し、構文・型をチェックし、動作するコードを生成します。すべてClaudeとの対話を通じて。
契約を定義する
エージェントが何をするかを平易な言語でClaudeに説明:
"ユーザー登録エージェントを定義して。ユーザー名とメールを受け取り、メールが@を含むか検証して、ユーザーIDを返す。ユーザー名は3～20文字である必要がある。"
Claudeは型、事前条件、事後条件、不変条件付きのVDM-SL仕様に加え、メッセージ型・状態遷移・APIシグネチャをまとめたPhase 2設計文書（PROTOCOL.md、API-SIGNATURES.md）も生成します。要件が曖昧な場合は確認質問をします。
仕様を検証する
仕様をチェックするようClaudeに依頼:
"この仕様を検証して"
VDMJが構文と型チェックを実行し、証明責務を生成します。あわせて設計文書の完全性と仕様との一貫性もチェックします。これは証明完了ではなく、必要に応じてZ3等で証明する対象を明示する段階です。Claudeは各POを平易な言葉で説明します。
コードを生成する
実装を生成するようClaudeに依頼:
"この仕様からTypeScriptコードを生成して"
Claudeはすべての事前条件、事後条件、不変条件がランタイムチェックにコンパイルされたTypeScript（またはPython）を生成します。契約が違反されると、違反された正確なルールを示すContractErrorが発生します。続けて"契約テストを生成して"と言えば、generate-testsスキルが仕様と設計文書から型不変式・事前/事後条件・状態遷移・境界値を網羅するJest/Vitestの契約テストを生成します。
ショートカット: "登録エージェントの完全ワークフローを実行して"と言えば、定義 → 構文・型チェック → 証明（必要な場合） → 生成 → テストの各フェーズを順に実行します。
主要概念
このプラグインを使うのに形式手法の知識は不要ですが、3つの概念を理解するとより効果的に使用できます:
事前条件
pre操作が実行される前に成立する必要があるルール。例: "タスクIDがボードに存在する必要がある。" 違反すると、呼び出し側が無効なリクエストを送った。
事後条件
post操作完了後に成立する保証。例: "削除後、タスクIDはボードに存在しない。" 違反すると、実装にバグがある。
不変条件
inv常に成立する必要があるルール。例: "タスクタイトルの長さ≤100文字。" レコード構築時にチェックされます。
プロンプトテンプレート
すぐに使えるプロンプトの雛形です。{...} の部分を自分のドメインに書き換えて使ってください。
テンプレート1: シンプル（単一エージェント）
最小限の情報で始めて、Claudeとの対話で深掘りするパターンです。
{エージェント名}エージェントを定義して。 【扱うデータ】 - {エンティティ}には{フィールド1}・{フィールド2}・{フィールド3}がある - {ステータスや列挙型があれば: ステータスは{値1}/{値2}/{値3}} 【やりたい操作】 - {操作1の説明} - {操作2の説明} 【守りたいルール】 - {ビジネスルール1} - {ビジネスルール2}
記入例: 在庫管理エージェント
在庫管理エージェントを定義して。 【扱うデータ】 - 商品には商品ID・商品名・在庫数・カテゴリがある - カテゴリは食品/日用品/家電 【やりたい操作】 - 入荷（指定数を在庫に加算） - 出荷（指定数を在庫から減算） - 在庫照会（商品IDで現在の在庫数を返す） 【守りたいルール】 - 在庫数は0未満にならない - 出荷数は現在の在庫数を超えられない - 商品名は空文字を許可しない
テンプレート2: マルチエージェント
複数エージェントが協調するシステム向け。エージェント間の依存関係を明示します。
以下のマルチエージェントシステムの契約を定義して。 【システム概要】 {システムが何をするか1〜2文} 【エージェント構成】 1. {Agent A名} — {役割の説明} 2. {Agent B名} — {役割の説明} 【エージェント間の依存】 - {Agent A}の{操作X}の完了後に{Agent B}の{操作Y}が呼ばれる 【共有するデータ型】 - {型名}: {フィールドの説明} 【各エージェントの主要ルール】 - {Agent A}: {制約} - {Agent B}: {制約}
記入例: EC注文処理システム
以下のマルチエージェントシステムの契約を定義して。 【システム概要】 ECサイトの注文処理。注文→在庫引当→決済の3エージェントが協調する。 【エージェント構成】 1. OrderAgent — 注文の受付・管理 2. InventoryAgent — 在庫の引当と解放 3. PaymentAgent — 決済処理 【エージェント間の依存】 - OrderAgentがConfirmOrderした後、InventoryAgentのReserveStockが呼ばれる - ReserveStock成功後、PaymentAgentのChargeが呼ばれる - Charge失敗時はInventoryAgentのReleaseStockで在庫を戻す 【各エージェントの主要ルール】 - OrderAgent: Paid状態の注文はキャンセルできない - InventoryAgent: 在庫数は0未満にならない - PaymentAgent: 与信確認済みでないと売上確定できない
テンプレート3: 統合ワークフロー（一気通貫）
定義→構文・型チェック→証明（必要な場合）→コード生成→テストを1コマンドで実行します。
統合ワークフローで{システム名}を開発して。 【ドメイン】 {何のためのシステムか} 【データ】 - {エンティティとそのフィールド} 【操作】 - {操作名}: {何をするか}（{事前条件があれば}） 【絶対に守るルール】 - {不変条件・ビジネスルール} 【生成言語】 {TypeScript / Python}
記入例: 会議室予約管理
統合ワークフローで予約管理システムを開発して。 【ドメイン】 会議室の予約管理。ダブルブッキングを仕様レベルで防ぎたい。 【データ】 - 会議室: 室ID・名前・定員 - 予約: 予約ID・室ID・開始時刻・終了時刻・予約者名 【操作】 - CreateReservation: 新規予約を作成（時間帯重複なし） - CancelReservation: 予約をキャンセル（予約が存在すること） 【絶対に守るルール】 - 同一部屋で時間帯が重なる予約は存在できない - 開始時刻 < 終了時刻 【生成言語】 TypeScript
テンプレート4: 既存仕様の形式化
すでに自然言語の仕様書やAPI定義がある場合、そのまま貼り付けて形式化します。
以下の仕様をVDM-SLの形式仕様に変換して。 --- {既存の仕様書やAPI定義をここに貼り付け} --- 特に以下の点を形式化してほしい: - {曖昧になりがちな箇所1} - {曖昧になりがちな箇所2} 形式化したら検証まで実行して。
テンプレート5: 契約テストの生成
検証済みの仕様（と設計文書）から実行可能な契約テストを生成します。
{仕様ファイル}から契約テストを生成して。 【入力】 - VDM-SL仕様: {パス} - {設計文書があれば: PROTOCOL.md / API-SIGNATURES.md のパス} 【出力】 - テストフレームワーク: {Vitest / Jest} - 対象実装: {テスト対象の実装ファイルパス} 型不変式・事前条件・事後条件・境界値{・状態遷移}のテストを網羅して。
プロンプトのコツ
- 「守りたいルール」を具体的に — 「在庫は0未満にならない」のように境界値を明示すると、精度の高い事前条件・不変条件が生成されます。
- エージェント間の呼び出し順序を明示 — 「A.post → B.pre」の関係がマルチエージェント契約の核心です。
- 最初から完璧を目指さなくてOK — テンプレート1で始めて、検証フェーズでClaudeが境界条件を質問してきます。
- 「統合ワークフローで」と付ければ一気通貫 — 定義→構文・型チェック→証明（必要な場合）→生成→テストが順に回り、エラー時は修正を支援します。
MD→VDM-SL→MDパイプライン
既存の不完全な仕様書（Markdown）を出発点に、VDM-SLへの変換を通じて曖昧性を体系的に検出・解消し、VDMJでチェックされたVDM-SLから自然言語仕様書を再生成するワークフローです。テンプレート4「既存仕様の形式化」の内部で動作する中核メカニズムでもあります。
パイプラインの核心
自然言語をVDM-SLに変換しようとする行為そのものが、仕様の曖昧性検出として機能します。型定義や事前条件・事後条件を書こうとしたとき「書けない箇所」が構造的に浮かび上がります。書けない理由は、元の自然言語仕様が曖昧だからです。
import-natural-spec
Markdown仕様を読み込み、VDM-SLへの変換を試行。変換できない箇所＝曖昧性として検出。
対話で曖昧性を解消
検出された曖昧性を優先度順にユーザーへ提示し、解釈を確定。
verify-spec
VDMJで構文・型チェック・証明責務（PO）生成を実行し、仕様の整合性を機械的にチェック。これはPOの証明完了を意味しません。
export-human-spec
VDMJでチェックされたVDM-SLを、ドメインエキスパートがレビュー可能な構造化Markdown仕様書に逆変換。
7つの曖昧性パターン
VDM-SLへの変換試行により、以下の7種類の曖昧性が構造的に露呈します:
- 曖昧な数量詞 —「複数」では型が定義できない（seq? set? 上限は?）
- 未定義の用語 —「アクティブ」の状態一覧が列挙されていない
- 暗黙の制約 — 代理注文の可否など、記述されていないルール
- 欠落したエラーケース — 支払い失敗時の動作が未定義
- 曖昧な関係 — 1対多か多対多かが不明
- 時間的曖昧性 — 処理順序の厳密さが不明
- 境界条件 — 包含か排他か（≤ vs <）が不明
優先度付き対話による解消
検出された曖昧性は3段階の優先度に分類され、ユーザーとの対話で順次解消されます。AIが曖昧性を暗黙的に解決することは決してなく、すべての解釈の選択がユーザーに提示されます。
ブロッキング — VDM-SLの型定義が書けない（最優先で解消）
重要 — 事前条件・事後条件に影響する
明確化 — 仕様をより精密にする
トレーサビリティとVDMJ検証
生成されるVDM-SL仕様は各要素に[REQ-nnn]タグと元の自然言語テキストをコメントとして保持し、元文書との双方向トレーサビリティを維持します。VDMJによる機械的チェック（構文チェック・型チェック・証明責務生成）の後、次のステップへ進みます。
自然言語仕様書への逆変換
VDMJでチェックされたVDM-SLを、ドメインエキスパートや非技術者がレビューできる構造化された仕様書に変換します。変換ルール:
types型定義 → 「何が存在するか」
pre事前条件（pre） → 「前提条件」
post事後条件（post） → 「保証」
inv不変条件（inv） → 「常に成立するルール」
この自然言語仕様書は派生成果物であり、VDM-SLが正（source of truth）です。ステークホルダーのレビューを経た修正要望はVDM-SLに反映→検証→再生成というサイクルを通ります。