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

AI Agent-Driven Development with Formal Methods

— The Human Role in the Era of Multi-Agent Collaboration —

A proposal for a new development paradigm where VDM-SL formal specifications serve as 'contracts' between AI agents, enabling multiple AI agents to collaborate like a team to autonomously build systems.

GitHub Repository →

Challenge: The 'Common Language' of Multi-Agent Collaboration

The era where AI writes code has already arrived. However, the next paradigm goes beyond 'using AI as a tool' to multiple AI agents collaborating like a team to autonomously build systems.

Here a fundamental question arises—when multiple AI agents collaborate, what becomes the 'team's common language'?

Proposal: Formal Specifications as 'Contracts' Between Agents

By using VDM-SL (Vienna Development Method - Specification Language) formal specifications as rigorous contracts between agents, the following can be achieved:

Parallel Autonomous Development

Each agent can independently develop with only its own module specification and dependent interface specifications. Implementation code from other modules is not required.

Mechanical Consistency Checking

Mechanical checking of A.post ⇒ B.pre composability. Properties selected for proof are handled separately as POs.

Structural Exposure of Ambiguity

Through type definitions, preconditions, postconditions, and invariants, interpretive discrepancies in natural language are made explicit and reduced.

Redefinition of Human Roles

Human roles are limited to domain experts. Focus on defining business rules and leave technology selection to AI.

Multi-Agent Architecture

Phase 1: Domain SpecificationHuman (Domain Expert) + Architect AI→ VDM-SL Formal Spec + @ext Annotations (NFRs) + Module Division→ Interface Contracts (A.post ⇒ B.pre)Agent AOrder ModuleContext:• Own module spec + @ext• Dependent IF spec onlyAgent BInventory ModuleContext:• Own module spec• Dependent IF spec onlyAgent CPayment ModuleContext:• Own module spec• Dependent IF spec onlyIntegration Verification AgentMechanically check A.post ⇒ B.pre across all modules(Does not inspect implementation code. Specification level only)

Concrete VDM-SL Specification Example

An example specification of the Order module. Preconditions, postconditions, and invariants function as the module's 'contract.'

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 <> [] -- Empty order not allowed post RESULT in set dom orders -- Order is registered and orders(RESULT).status = <PENDING> -- Initial status is PENDING ConfirmOrder: OrderId ==> () ConfirmOrder(orderId) == ... pre orderId in set dom orders -- Order exists and orders(orderId).status = <PENDING> -- Only PENDING state can be confirmed post orders(orderId).status = <CONFIRMED> -- ← Contract to Inventory module

The postcondition of ConfirmOrder status = <CONFIRMED> satisfies the precondition that ShipOrder in the Inventory module requires order.status = <CONFIRMED>. This is the target of an A.post ⇒ B.pre contract-consistency check. The @ext annotation expresses non-functional requirements (performance, availability, usability, etc.) that cannot be expressed in VDM-SL, and serves as input for AI's technology selection in Phase 2.

Comparison with Existing AI-Driven Development Approaches

Each existing major AI-driven development architecture has distinct strengths, but they all harbor structural flaws in their 'source of truth.'

MethodSource of TruthStructural Flaw
Devin / SWE-AgentExisting code behaviorCircular reasoning Inferring specs from code entrenches bugs
MetaGPTSOP + natural language documentsAmbiguity accumulation NL degradation compounds per phase
ChatDevChat Chain dialogue consensusNon-reproducible Different outputs for same input
GitHub Spec KitStructured MarkdownStructured ambiguity Implicit boundary conditions
Claude Code, etc.Developer judgmentCannot scale Limit of cognitive load
Our MethodVDM-SL formal specificationLimited scope Not suited for UI/UX or lightweight tasks

Detailed Structural Flaws of Each Approach

Positioning Map

Single AgentMulti-AgentDeductive Verification (Proved Scope)Inductive Verification (Test Dependent)Single × InductiveMulti × DeductiveSingle × InductiveMulti × InductiveDevinSWE-AgentCursor / CopilotMetaGPTChatDevSpec Kit(Structured NL, intermediate)★ Our MethodFormal-Spec-Driven

Our method is positioned in the upper-right quadrant — Multi-Agent × specification verification with proof targets.

The New Role of Humans

In this paradigm, the human role is limited to domain expert. Defining business rules and non-functional requirements (@ext annotations) is the human's job, while technology selection (language, framework, DB) and architecture design are performed autonomously by AI in Phase 2.

Before

Traditional Developer

  • Write code
  • Write tests
  • Review code
  • Debug integration bugs
After

Humans in the AI Agent Era

  • Define business rules (Phase 1)
  • Quantify NFRs with @ext annotations
  • Evaluate and judge AI's specification explanations
  • Delegate technology selection and implementation to AI (Phase 2+)

There is no need to read or write formal notation. AI agents handle that. Humans, as domain experts, make judgments on the content explained in natural language by the Architect AI, such as 'Is this module division appropriate for this specification?' Whether to use Python, Ruby, or TypeScript is not the domain expert's concern—in Phase 2, AI autonomously selects the optimal technology based on @ext annotations.

How to Practice with Claude Code

Claude Code's CLAUDE.md hierarchical loading mechanism naturally corresponds to the scope separation of formal-spec-driven development. By placing overall contracts at the root and module specifications in each module directory, you can keep the context for each session minimal.

Recommended Directory Structure

project-root/ ├── CLAUDE.md ← Overall contract + @ext rules (always loaded) ├── .claude/rules/ │ ├── specification-phase.md ← Phase 1: rules for spec editing │ ├── design-phase.md ← Phase 2: design rules (AI autonomous) │ └── implementation-phase.md← Phase 3: implementation rules (AI autonomous) ├── specs/ │ ├── shared-types.vdmsl ← Common type definitions │ ├── order-interface.vdmsl ← IF contract + @ext annotations │ └── ... └── modules/ ├── order/ │ ├── CLAUDE.md ← Module spec (lazy loaded) │ └── src/ ← Implementation in AI-selected tech ├── inventory/ │ ├── CLAUDE.md │ └── src/ └── payment/ ├── CLAUDE.md └── src/
Root

Overall Contract

Describes module dependencies, shared type definitions, A.post ⇒ B.pre rules, and @ext annotation conventions. Always loaded in all sessions.

Per Module

Spec + Dependent IF

Own module specification + dependent interface contracts only. Lazy-loaded only when files in that directory are accessed.

Path Rules

Phase-specific Rules

Automatically switches Claude Code behavior rules between editing specs/** and modules/*/src/**.

Parallel Development Execution Example

# Terminal 1: Order module (Phase 2: AI autonomous - tech selection → design → implementation) cd project-root/modules/order/ && claude # → Root CLAUDE.md + Order spec (@ext included) + Inventory/Payment IF contracts # Terminal 2: Inventory module (parallel, AI autonomous) cd project-root/modules/inventory/ && claude # → Root CLAUDE.md + Inventory spec (@ext included) + Order IF contract # Terminal 3: Integration check (AI autonomous) cd project-root/integration/ && claude # → Load all IF specs, check A.post ⇒ B.pre + @ext compliance

Each session develops without seeing each other's implementation code, using only interface contracts. Even if Order is implemented on Monday and Inventory on Friday, the formal specifications in CLAUDE.md make cross-session consistency mechanically checkable.

MethodWhat enters the contextEstimated lines
Natural language spec (bulk)Requirements documents for all modules500–2,000 lines
CLAUDE.md + VDM-SLRoot contract + own module spec + dependent IF100–300 lines

Resources

Paper (Japanese / English)

Detailed in paper format: theoretical foundations, workflow, and roadmap for formal-spec-driven development.

Japanese → / English →

Comparative Analysis

Systematic comparison with MetaGPT, ChatDev, Devin, Spec Kit, etc., and structural flaw analysis of each approach.

Comparative Analysis →

Claude Code Practice Guide

Concrete development methods leveraging CLAUDE.md's hierarchical structure. Directory structure, workflow, and context optimization.

Practice Guide →

Prompt Templates

Supports all phases from Phase 1-4. Ready to copy & paste into Claude/GPT-4.

Templates →

Implementation Example (EC Site)

A sample that defines specifications for three modules—order, inventory, and payment—in VDM-SL and builds them with multi-agent development.

Sample →

ANDO Hikaru — IID Systems — Apache License 2.0

← Back to Overview