Formal Model of Agent Coupling: Verified Coordination Under Byzantine Conditions

This paper presents the formal model underpinning the Agent Coupling Protocol. We develop a process calculus for agent interaction — the Agent Interaction Calculus (AIC) — and prove that ACP achieves verified coordination under Byzantine conditions with O(log n) attestation overhead. We derive the necessary and sufficient conditions for coordination liveness and prove termination bounds for nested delegation chains.