Contraction Contracts: Enforced Progress Guarantees for Black-Box Agent Loops

Abstract

The verify-and-revert loop -- propose, apply, keep only if a measured quantity improved, otherwise roll back -- is folk practice in agent engineering, with no design methodology and no guarantees. We adapt Kolesnikov's Analytical Design of Aggregated Regulators to plants that admit no invertible model: where classical ADAR substitutes the plant into a contraction equation and solves for the control, the harness enforces that equation on realised transitions. The loop then carries its own certificate in two grades: pathwise termination assumes nothing and holds against arbitrary, even adversarial, model behaviour, while a tight success bound in which the budget for neutral moves does not appear and a closed form for expected proposals hold given a per-state controllability floor -- the only place model and prompt enter, and a quantity traces refute but never certify. On program repair, an arm shown exactly what the contract is shown and required to act on none of it ends worse than it started in 79.4% and 80.0% of runs on two oracles, against 0.0% for the contract: enforcement, not measurement, is what makes the loop safe, and even best-of-n, which keeps nothing and so cannot keep damage, is as safe as the full contract. Measuring the controllability function gives the other result: rollback issues a step's retries from one state, per-state success probabilities are close to bimodal, and a capability profile therefore transfers to smaller retry budgets r but not to larger ones -- fitting at r = 2 over-predicts r = 8 by 2.1x, fitting at r = 8 under-predicts r = 2 by 2.0x.