IID.systems
ProfileServicesFormal MethodsAI AlignmentEssaysBookSchoolGitHub↗日本語
日本語
ResearchOpen Source

AI Agent-Driven Development Using Formal Methods

— Role of Humans in the Multi-Agent Collaboration Era —

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

GitHub Repository →

Challenge: "Common Language" for Multi-Agent Collaboration

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

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

Proposal: Formal Specification as "Contract" Between Agents

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

Parallel Autonomous Development

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

Mechanical Consistency Checking

A.post ⇒ B.pre の合成可能性をツールで機械的にチェック。 証明対象の性質は別途POとして扱います。

Structural Exposure of Ambiguity

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

Redefinition of Human Roles

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

Multi-Agent Architecture

Phase 1: Domain Specification DraftingHuman (domain expert) + Architect AI→ VDM-SL formal specification + @ext annotations (non-functional requirements) + module division→ インターフェース契約 (A.post ⇒ B.pre)Agent AOrder Moduleコンテキスト:・自モジュール仕様 + @ext・依存先 IF 仕様のみAgent BInventory Moduleコンテキスト:・自モジュール仕様・依存先 IF 仕様のみAgent CPayment Moduleコンテキスト:・自モジュール仕様・依存先 IF 仕様のみIntegration Verification Agent全モジュールの A.post ⇒ B.pre を機械的チェック(Does not view implementation code. Specification level only)

VDM-SL Specification Example

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

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が技術選定を行う際の入力となる。

Comparison with Existing AI-Driven Development Approaches

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

Detailed Critique of Each Approach

Positioning Map

Single AgentMulti-AgentDeductive Verification (Proved Scope)Inductive Verification (Test Dependency)単一×帰納マルチ×演繹単一×帰納マルチ×帰納DevinSWE-AgentCursor / CopilotMetaGPTChatDevSpec Kit(Structured NL, intermediate)★ This MethodFormal-Spec-Driven

This approach sits in the lower right quadrant — Multi-Agent × specification verification with proof targets.

New Human Role

このパラダイムにおいて、人間の役割はドメインエキスパートに限定されます。業務ルールと非機能要件（@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 Integration

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

Recommended Directory Structure

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/
Root

Full Contract

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

Module

Specification + Dependent IF

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

Path Rules

Path-based Rules

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

Parallel Development Execution Example

# ターミナル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の形式仕様によりセッション間の整合性が保たれる。

Resources

論文（日本語 / 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