cobound-validator

Pre-deployment coordination feasibility checker for multi-agent AI systems — backed by 2,433 formally verified Lean 4 theorems.

Core theorem: H¹(K;ℤ) = 0 if and only if the multi-agent communication graph is acyclic (a forest).
Cycles create cohomological obstructions that make coordination mathematically impossible.
Source: h1_trivial_iff_oneConnected — MultiAgent/ScalableH1.lean

---

Installation

pip install cobound-validator

---

Quick Start

YAML topology file

# topology.yaml
agents:
  - id: coordinator
  - id: worker-1
  - id: worker-2
edges:
  - from: coordinator
    to: worker-1
  - from: coordinator
    to: worker-2

Run the validator

cobound-validate topology.yaml

Expected output (acyclic — passes)

╔══════════════════════════════════════════════════════════════╗
║          COBOUND VALIDATOR — Coordination Check              ║
╚══════════════════════════════════════════════════════════════╝

  Agents: 3   Edges: 2
  Theorem: h1_trivial_iff_oneConnected

  VERDICT: ✓ COORDINATION FEASIBLE (H¹ = 0)

  Mathematical basis: H¹(K;ℤ) = 0 ⟺ coordination feasible
  [Theorem: delta_squared_zero]
  Source: github.com/coboundinc/cobound (2,433 verified theorems)

Python API

from cobound_validator import validate

result = validate("topology.yaml")
print(result["feasible"])       # True
print(result["cycles"])         # []
print(result["mast_failures"])  # []

---

Example Topologies

✓ MetaGPT Assembly Line (examples/metagpt_assembly_line.yaml)

A linear software-development pipeline: product-manager → architect → engineers → QA → tech-writer.
No cycles. VERDICT: ✓ COORDINATION FEASIBLE (H¹ = 0)

cobound-validate examples/metagpt_assembly_line.yaml

---

✗ ChatDev Review Cycle (examples/chatdev_review_cycle.yaml)

A ChatDev-style pipeline where the reviewer sends code back to the programmer, creating a cycle.
VERDICT: ✗ COORDINATION OBSTRUCTED (H¹ ≠ 0)

cobound-validate examples/chatdev_review_cycle.yaml

---

✓ Star Topology (examples/star_topology.yaml)

One coordinator dispatches tasks to independent worker agents and collects results.
No worker communicates with another. VERDICT: ✓ COORDINATION FEASIBLE (H¹ = 0)

cobound-validate examples/star_topology.yaml

---

CLI Reference

Usage: cobound-validate [OPTIONS] [INPUT]

  Check a multi-agent topology for coordination feasibility.

  INPUT is a file path or '-' to read from stdin.

Options:
  --format [text|json]  Output format.  [default: text]
  --strict              Exit with code 1 even on a single cycle.
  --version             Show the version and exit.
  --help                Show this message and exit.

Exit codes:
  0   Coordination feasible (no cycles)
  1   Coordination obstructed (cycles detected)
  2   Error (invalid input or parse failure)

JSON output

cobound-validate topology.yaml --format json

{
  "feasible": false,
  "agent_count": 4,
  "edge_count": 5,
  "cycles": [["agent-A", "agent-B", "agent-C", "agent-A"]],
  "mast_failures": [
    {"failure_mode": "FM-3.1", "label": "Infinite coordination loops", "percentage": 8.9, "affected_agents": ["agent-A", "agent-B", "agent-C"]},
    ...
  ],
  "suggested_fixes": [
    {"remove_edge": ["agent-B", "agent-C"], "breaks_cycles": 1, "new_topology": "forest"}
  ]
}

GitHub Action

- name: Validate agent topology
  uses: insinuateai/cobound-validator@v0.1.0
  with:
    topology_file: path/to/topology.yaml
    fail_on_obstruction: "true"

---

MAST Failure Modes

When cycles are detected, cobound-validator maps them to empirically observed failure modes from the MAST taxonomy (NeurIPS 2025):

Code	Failure Mode	Frequency
FM-1.1	Context window overflow	11.8%
FM-1.3	Lost in the middle	15.7%
FM-1.5	Task specification error	12.4%
FM-2.1	Hallucination propagation	9.3%
FM-3.1	Infinite coordination loops	8.9%

Reference: "MAST: A Multi-Agent System Taxonomy for LLM-based Pipelines", NeurIPS 2025.

---

Mathematical Foundation

The correctness of this tool is grounded in algebraic topology. For a simplicial complex K modelling a communication network:

H¹(K;ℤ) = 0  ⟺  K has no 1-cycles  ⟺  the underlying graph is a forest

This equivalence — and the algorithmic consequences for multi-agent systems — is formally proved in 2,433 Lean 4 theorems at:

github.com/coboundinc/cobound

Key theorem: h1_trivial_iff_oneConnected in MultiAgent/ScalableH1.lean

---

License

MIT © Kian Quinlan / Insinuate AI