IID.systems
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 の合成可能性をツールで自動検証。 エージェント数が増えても検証コストは線形。

曖昧性の構造的排除

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

人間の役割の再定義

人間はドメインエキスパート＋アーキテクチャ決定者へ。 コードではなく「何を作るか」に集中。

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

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

VDM-SL仕様の具体例

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

module Order 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 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 の機械的検証。

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

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

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

ポジショニングマップ

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

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

人間の新しい役割

このパラダイムにおいて、人間はドメインエキスパートかつ アーキテクチャレベルの意思決定者です。

Before

従来の開発者

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

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

  • ビジネスルールを定義する
  • システム全体の分割を設計する
  • AIの仕様説明を評価・判断する
  • エージェントチームの成果を監督する

形式記法を読み書きする必要はありません。それはAIエージェントが担います。 人間は、アーキテクトAIが「この仕様でモジュール分割は適切ですか？」と 自然言語で説明した内容に対して、ドメインエキスパートとして判断を下します。

リソース

論文（日本語 / English）

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

日本語版 → / English →

比較分析

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

比較分析 →

プロンプトテンプレート

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

テンプレート →

実装例（ECサイト）

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

サンプル →

Hikaru Ando — IID Systems — Apache License 2.0