Contract-Governed Multi-Agent Graph Orchestration for Long-Horizon Autonomous Research Pipelines

Long-horizon autonomous research systems now execute multi-stage workflows with planner, tool, and reviewer modules, yet most guarantees remain local or empirical. We formalize a contract-governed orchestration model in which execution is a finite directed acyclic phase graph with typed interfaces, adapter maps, decidable transition guards, and validator-mediated control. Within this setting, we define a safety objective that minimizes contract violations and a recoverability objective that minimizes halting time under bounded control. We prove a graph-level safety theorem by composing edge admissibility and invariant propagation, and we prove a bounded recoverability theorem with an explicit finite halt envelope; we also prove an impossibility boundary when boundedness or monotone escalation is removed. The formal statements are paired with theorem-audit evidence from symbolic checks and seeded trace sweeps: fail-closed bounded runs satisfy the proven envelope, while fail-open or non-monotone regimes produce counterexamples exactly where the theory predicts failure. The resulting manuscript gives a theorem-first blueprint for contract-compositional orchestration that separates theorem-supported claims from diagnostic, out-of-regime observations.