IID.systems
ProfileServicesFormal MethodsSchoolGitHub↗
ResearchOpen Source

形式手法によるAIエージェント駆動開発

— マルチエージェント協調時代における人間の役割 —

VDM-SL形式仕様をAIエージェント間の「契約」として機能させ、 複数のAIエージェントがチーム開発のように協調してシステムを自律構築する 新しい開発パラダイムの提案。

GitHub Repository →

課題：マルチエージェント協調の「共通言語」

AIがコードを書く時代は既に到来しています。しかし、次のパラダイムは 「AIをツールとして使う」段階を超え、複数のAIエージェントがチーム開発のように 協調し、システムを自律的に構築することです。

ここで根本的な問いが生じます——複数のAIエージェントが協調するとき、 何が「チームの共通言語」になるのか？

提案：形式仕様をエージェント間の「契約」に

VDM-SL（Vienna Development Method - Specification Language）の形式仕様を エージェント間の厳密な契約として使うことで、以下が実現できます。

並行自律開発

各エージェントは自モジュール仕様＋依存先IF仕様のみで独立に開発可能。 他モジュールの実装コードは不要。

機械的整合性検証

A.post ⇒ B.pre の合成可能性をツールで自動検証。 エージェント数が増えても検証コストは線形。

曖昧性の構造的排除

型定義・事前条件・事後条件・不変条件により、 自然言語の解釈の齟齬を原理的に排除。

人間の役割の再定義

人間の役割はドメインエキスパートに限定。 業務ルールの定義に集中し、技術選定はAIに委ねる。

マルチエージェントアーキテクチャ

Phase 1: ドメイン仕様策定人間（ドメインエキスパート）＋ アーキテクトAI→ VDM-SL形式仕様 ＋ @ext注釈（非機能要件）＋ モジュール分割→ インターフェース契約 (A.post ⇒ B.pre)Agent A注文モジュールコンテキスト:・自モジュール仕様 + @ext・依存先 IF 仕様のみAgent B在庫モジュールコンテキスト:・自モジュール仕様・依存先 IF 仕様のみAgent C決済モジュールコンテキスト:・自モジュール仕様・依存先 IF 仕様のみ統合検証エージェント全モジュールの A.post ⇒ B.pre を機械的検証（実装コードは見ない。仕様レベルのみ）

VDM-SL仕様の具体例

注文モジュールの仕様例。事前条件・事後条件・不変条件が モジュールの「契約」として機能します。

module Order -- @ext:performance { latency: "< 200ms p99", throughput: "1000 req/s" } -- @ext:availability { uptime: "99.9%", maintenance_window: "02:00-04:00 JST" } -- @ext:usability { criterion: "8/10 users complete checkout in < 3 min" } types OrderId = nat1; ProductId = nat1; LineItem :: productId : ProductId quantity : nat1 unitPrice : nat; OrderStatus = <PENDING> | <CONFIRMED> | <COMPLETED> | <CANCELLED>; state OrderStore of orders : map OrderId to Order nextOrderId : nat1 inv mk_OrderStore(orders, nextOrderId) == nextOrderId > 0 and forall id in set dom orders & orders(id).orderId = id operations -- @ext:scalability { peak: "10x normal traffic", strategy: "horizontal" } CreateOrder: nat1 * seq of LineItem ==> OrderId CreateOrder(customerId, items) == ... pre items <> [] -- 空注文は不可 post RESULT in set dom orders -- 注文が登録される and orders(RESULT).status = <PENDING> -- 初期状態はPENDING ConfirmOrder: OrderId ==> () ConfirmOrder(orderId) == ... pre orderId in set dom orders -- 注文が存在する and orders(orderId).status = <PENDING> -- PENDING状態のみ確認可 post orders(orderId).status = <CONFIRMED> -- ← 在庫モジュールへの契約

ConfirmOrder の事後条件 status = <CONFIRMED> は、 在庫モジュールの ShipOrder の事前条件が要求するorder.status = <CONFIRMED> を満たす。 これが A.post ⇒ B.pre の機械的検証。@ext 注釈はVDM-SLでは表現できない非機能要件（性能、可用性、ユーザビリティ等）を 形式的に記述し、Phase 2でAIが技術選定を行う際の入力となる。

既存AI駆動開発手法との比較

既存の主要なAI駆動開発アーキテクチャはそれぞれ明確な強みを持つ一方、 「正しさの根拠（source of truth）」に構造的な欠陥を抱えています。

各手法の構造的欠陥の詳細

ポジショニングマップ

単一エージェントマルチエージェント演繹的検証（仕様保証）帰納的検証（テスト依存）単一×帰納マルチ×演繹単一×帰納マルチ×帰納DevinSWE-AgentCursor / CopilotMetaGPTChatDevSpec Kit（構造化NL・中間）★ 本手法Formal-Spec-Driven

本手法は右下の象限——マルチエージェント × 演繹的検証——に位置する唯一のアプローチ。

人間の新しい役割

このパラダイムにおいて、人間の役割はドメインエキスパートに限定されます。業務ルールと非機能要件（@ext注釈）を定義するのが人間の仕事であり、 技術選定（言語・フレームワーク・DB）やアーキテクチャ設計はPhase 2でAIが自律的に行います。

Before

従来の開発者

  • コードを書く
  • テストを書く
  • コードレビューする
  • 統合バグをデバッグする
After

AIエージェント時代の人間

  • ビジネスルールを定義する（Phase 1）
  • 非機能要件を@ext注釈で定量化する
  • AIの仕様説明を評価・判断する
  • 技術選定・実装はAIに委ねる（Phase 2+）

形式記法を読み書きする必要はありません。それはAIエージェントが担います。 人間は、アーキテクトAIが「この仕様でモジュール分割は適切ですか？」と 自然言語で説明した内容に対して、ドメインエキスパートとして判断を下します。 「PythonかRubyかTypeScriptか」はドメインエキスパートの関心事ではなく、 Phase 2でAIが@ext注釈に基づいて自律的に最適な技術を選択します。

Claude Code での実践方法

Claude CodeのCLAUDE.md階層ロード機構は、 形式仕様駆動開発のスコープ分離と自然に対応します。 ルートに全体契約、各モジュールディレクトリにモジュール仕様を配置することで、 各セッションのコンテキストを最小限に保てます。

推奨ディレクトリ構成

project-root/ ├── CLAUDE.md ← 全体契約 + @ext規約（常時ロード） ├── .claude/rules/ │ ├── specification-phase.md ← Phase 1: 仕様編集時の規約 │ ├── design-phase.md ← Phase 2: 設計時の規約（AI自律） │ └── implementation-phase.md← Phase 3: 実装時の規約（AI自律） ├── specs/ │ ├── shared-types.vdmsl ← 共通型定義 │ ├── order-interface.vdmsl ← IF契約 + @ext注釈 │ └── ... └── modules/ ├── order/ │ ├── CLAUDE.md ← モジュール仕様（遅延ロード） │ └── src/ ← AI選定の技術で実装 ├── inventory/ │ ├── CLAUDE.md │ └── src/ └── payment/ ├── CLAUDE.md └── src/
ルート

全体契約

モジュール依存関係、共通型定義、A.post ⇒ B.preルール、@ext注釈規約を記述。 全セッションで常時ロード。

モジュール別

仕様 + 依存先IF

自モジュール仕様＋依存先インターフェース契約のみ。 そのディレクトリのファイルに触れた時だけ遅延ロード。

パス別ルール

フェーズ別規約

specs/**編集時とmodules/*/src/**編集時で Claude Codeの行動規約を自動切替。

並列開発の実行例

# ターミナル1: Orderモジュール（Phase 2: AI自律で技術選定→設計→実装） cd project-root/modules/order/ && claude # → ルートCLAUDE.md + Order仕様(@ext含む) + Inventory/Payment IF契約 # ターミナル2: Inventoryモジュール（並列、AI自律） cd project-root/modules/inventory/ && claude # → ルートCLAUDE.md + Inventory仕様(@ext含む) + Order IF契約 # ターミナル3: 統合検証（AI自律） cd project-root/integration/ && claude # → 全IF仕様を読み込み、A.post ⇒ B.pre + @ext準拠を検査

各セッションは互いの実装コードを見ず、インターフェース契約のみで開発。 月曜にOrderを実装し金曜にInventoryを実装しても、 CLAUDE.mdの形式仕様によりセッション間の整合性が保たれる。

リソース

論文（日本語 / English）

形式仕様駆動開発の理論的根拠、ワークフロー、ロードマップを 論文形式で詳述。

日本語版 → / English →

比較分析

MetaGPT、ChatDev、Devin、Spec Kit等との 体系的比較と各手法の構造的欠陥分析。

比較分析 →

Claude Code実践ガイド

CLAUDE.mdの階層構造を活用した具体的な開発方法。 ディレクトリ構成、ワークフロー、コンテキスト最適化。

実践ガイド →

プロンプトテンプレート

Phase 1-4の全フェーズ対応。コピー＆ペーストで Claude/GPT-4に投入可能。

テンプレート →

実装例（ECサイト）

注文・在庫・決済の3モジュールをVDM-SLで仕様定義し、 マルチエージェントで構築するサンプル。

サンプル →

Hikaru Ando — IID Systems — Apache License 2.0

← 概要に戻る