IID.systems
プロフィール事業紹介形式手法AIアライメントエッセイ書籍プログラミング教室GitHub↗English
English
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 の合成可能性をツールで機械的にチェック。証明対象の性質は別途POとして扱います。

曖昧性の構造的明示

型定義・事前条件・事後条件・不変条件により、自然言語の解釈の齟齬を構造的に明示し低減。

人間の役割の再定義

人間の役割はドメインエキスパートに限定。業務ルールの定義に集中し、技術選定は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）」に構造的な欠陥を抱えています。

手法正しさの根拠構造的欠陥
Devin / SWE-Agent既存コードの挙動循環論法 コードからの仕様推測がバグを固定化
MetaGPTSOP + 自然言語ドキュメント曖昧性蓄積 NLの劣化がフェーズごとに加算
ChatDevChat Chain対話合意再現不可能 同一入力で異なる出力
GitHub Spec Kit構造化Markdown構造化された曖昧性 境界条件の暗黙化
Claude Code等開発者の判断スケーリング不能 認知的負荷の限界
本手法VDM-SL形式仕様適用範囲限定 UI/UX・軽量タスクには不向き

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

ポジショニングマップ

単一エージェントマルチエージェント演繹的検証（証明対象）帰納的検証（テスト依存）単一×帰納マルチ×演繹単一×帰納マルチ×帰納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の形式仕様によりセッション間の整合性をチェックできる。

方式コンテキストに入るもの推定行数
自然言語仕様一括全モジュールの要件定義書500〜2,000行
CLAUDE.md + VDM-SLルート契約 + 自モジュール仕様 + 依存先IF100〜300行

リソース

論文（日本語 / English）

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

日本語版 → / English →

比較分析

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

比較分析 →

Claude Code実践ガイド

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

実践ガイド →

プロンプトテンプレート

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

テンプレート →

実装例（ECサイト）

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

サンプル →

ANDO Hikaru — IID Systems — Apache License 2.0

← 概要に戻る