escrow-budget

That total spend never exceeds the cap in any reachable state of the escrow protocol, in Lean, for any finite set of replicas and any non-negative amounts.

The bound, not conservation. No liveness, availability, or Byzantine model; crash is global in the Lean model. No machine-checked refinement connects the Lean proof, the TLA+ model, and the Python harness, their agreement is bounded, at one configuration, not a refinement.

Induction over the reachable states for an arbitrary finite roster, with the budget bound as the invariant; cross-checked by a TLA+ model and a Python fault harness that exercise crash and recovery the proof does not cover.

The theorems reachable_safe and durable_reachable_safe prove the bound; the axiom audit reports only propext and Quot.sound; a fault harness holds over 10,000 executions.

The Lean 4 kernel (v4.32.0), mathlib-free; the axioms used are propext and Quot.sound only, with no user axioms and no sorry. Plus the transition system being a faithful abstraction of the protocol, which is argued, not machine-proved.

Escrow and budget protocols; assume-guarantee reasoning. The contribution is the machine-checked unbounded budget bound and the first-person audited account of where its three methods are complementary, not confirmatory.

make clean && make check

Findings drawn from this artifact are on the evidence ledger.