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

Abstract

Long-horizon research automation needs stronger semantics than prompt chaining or schema-only artifact passing. We study a restricted contract-governed formulation of Quarks in which a finite active workflow branch is modeled as a typed directed acyclic graph, each node carries explicit assumptions and guarantees over artifact spaces, cross-node transport is mediated by sound adapters and admissible aggregators, and execution state is split into a global append-only provenance ledger and branch-local working memory. Within that regime we prove three results. First, typed local admissibility composes over the branch when the contract premises hold. Second, branch isolation and provenance monotonicity follow from the append-only, non-merge memory discipline. Third, local validator passes do not imply unrestricted graph-level correctness: we construct a two-node counterexample and then prove a narrow positive corollary for a manuscript-defined typed property class under explicit coverage, adapter, and memory assumptions. The proof package is complemented by seeded finite theorem audits and implementation-alignment checks against the Quarks architecture context. The positive audit families close completely in the declared regime, with 40/40 contract-composition cases, 45/45 memory cases, and 15/15 restricted-assurance cases passing; each theorem also retains a nontrivial archive of negative witnesses outside the proved setting. The result is a bounded but useful semantics for research orchestration: it supports typed admissibility, provenance discipline, and limited assurance claims without upgrading branch merges, semantic quality, or unrestricted agent competence into theorem-level guarantees.