The Composition Tax
A Verified Invariant and an Agent Contract for Safe Multi-MCP Workflows
The results apply only to the disclosed proxy, schemas, trials, and frozen baselines.
Abstract
When two MCP servers compose into a multi-agent workflow, the arrangement carries a composition tax: a structural cost in undetected convention mismatches that schema validation does not see. This paper assembles a four-layer chain that makes the tax visible. (1) Math: the witness rank r is the unique numerical invariant on compositional carriers with disclosure satisfying four structural axioms (Theorem 5.1), with proof bodies verified by the Lean 4 compiler against pinned Mathlib. (2) Tool: we ship Bulla, a live MCP proxy that computes r from raw tools/list responses with no manual composition construction, recovering 88% of obstructions on the canonical multi-server pair. (3) Behavior: across 78 trials over four rounds, a 3-sentence MANDATORY POLICY system prompt drives agents to consult r before cross-server calls (Claude 100%, GPT-4o 67%); a polite framing produces 0%. (4) Discipline: two design directions were tested against pre-registered criteria and falsified — producer-side response annotation, and voluntary consultation via polite prompts — and are documented alongside what survives.
Evidence and record
What does the live proxy report about the cost of semantic composition?
The witness rank is the unique invariant (Lean-verified); the live proxy recovers 88% from raw schemas; MANDATORY POLICY produces 100% consultation on Claude (0% with polite framing); two design alternatives pre-registered and killed
Reproduction failure or a frozen cheap baseline matching the reported result.
not requested