A spending cap was proved to hold in every reachable state of a protocol model.

Can total spend exceed its cap in any reachable state of the modelled escrow protocol?

Tests check the states someone thought to run. A cap in a replicated system has to hold in states nobody tested: after crashes, duplicated messages and recovery. Only a proof over all reachable states says that, and only for the model it is about.

Proved: A machine-checked proof exists for the stated model and property. Model-bounded: True of a model. Whether the model matches an implementation is a separate question.

1. Wrote a transition model of the protocol (charge, send, receive, drop, crash, recover) and stated the budget bound as an invariant.
2. Proved it by induction over reachable states in Lean 4: reachable_safe without crashes, durable_reachable_safe with global crash and recovery.
3. Proved four negative-control theorems showing that the guards are load-bearing.
4. Cross-checked with bounded TLA+ models, including deliberately broken variants, and with 10⁴ composed-fault runs of a Python implementation.

• Both safety theorems are recorded in the repository’s theorem index as checked by the Lean kernel with no project-defined axioms and no sorry, relying only on Lean’s standard propext and Quot.sound.
• Each negative control holds: skip the write-ahead debit, make receiver deduplication volatile, drop the in-flight non-negativity, or restore state without phase discipline, and the bound breaks.
• The broken TLA+ variants produce counterexamples, as they must; mutation suites kill 12 of 12 injected faults.

The objections that would most easily undo the conclusion, and what answered each.

Could the proof be vacuous, true because the model allows nothing?

Four negative-control theorems show the bound fails when a guard is removed, so the guards carry the proof.

Does it depend on hidden assumptions?

The assumptions (duplicate-free rosters, natural-number amounts, a genesis replica) are stated in the theorems.

Does the model match an implementation?

Not established. Bounded TLA+ checks and 10⁴ composed-fault runs of a Python implementation agree with it; the correspondence itself is argued, not proved.

The proof is about this model and this invariant. It is not a proof that any implementation is correct.

THEOREM-INDEX.md lists every theorem, its assumptions and its grade. The command is given as the repository documents it; it was not re-run for this page.