Proof-Carrying Agent Contracts (PACT): Governed Release for Stateful Agent Execution

Tool-using agents are usually judged by task completion, even though the side effects that produce a successful result must also satisfy authority, budget, interface, and recovery constraints at execution time. Proof-Carrying Agent Contracts (PACT) treats this commit boundary as a separate control problem. A typed contract binds an action graph to scoped authority, budget rules, admissible interfaces, declared recovery paths, proof obligations, and accountability evidence. At commit time, a trusted gate rechecks live-dependent obligations and records the decision in an attested release record. Under explicit assumptions on policy coverage, local-verifier soundness, and trusted commit binding, released actions are policy-admissible; structural refinement can only shrink the release set; and dependency-complete cache reuse is equivalent to recomputing reused checks. VeraContract-Bench adds deployment constraints to 180 autonomous software-engineering task instances and evaluates matched runs at both action and task levels. With three matched seeds for stochastic methods, PACT attains 63.5% task success with 1.8% unsafe-release rate, compared with 64.1% and 19.3% for the matched ReAct backbone. Governed success reaches 49.3%, versus 37.2% for AgentSpec-style runtime rules; recovery reaches 79.4%, and release-gate P99 latency is 64 ms. These results separate successful task completion from deployable execution at the commit boundary.