Findings · Formal verification

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

Evidence

The safety property is the bound, the sum of spend across replicas staying within the cap, and it is proved by induction over the reachable states for an arbitrary finite roster. The repository is careful about what the three methods around it do and do not do: the Lean proof is unbounded, the model checker and the fault harness are bounded, and their agreement is bounded agreement at one configuration, not a refinement. Remove the write-ahead debit or the durable receiver dedup and the proof breaks, the negative controls check that the discipline carries the bound.

Sample. Universal over any finite replica set and any cap including zero. Two standard axioms, propext and Quot.sound; no user axioms, no sorry. Negative controls show the discipline is load-bearing, and a fault harness holds over 10,000 executions.

Boundary

The bound, not conservation. No liveness, availability, or Byzantine model; crash is global in the Lean model, and per-replica crash is only exercised in the bounded checks. The proof holds relative to the transition system being a faithful abstraction of the protocol, which is argued, not machine-checked.

Independent reproduction. None known.

Reproduction

make clean && make check

Toolchain: Lean 4 leanprover/lean4:v4.32.0 (mathlib-free); TLA+ Tools v1.7.4; Python 3 with Hypothesis
Expected output: the axiom audit reports only propext and Quot.sound; positive models hold; the negative-control models produce their counterexamples
Claim stated at: repowazdogz-droid/escrow-budget · lean/Escrow/Reachability.lean:31-35
Verified at: repowazdogz-droid/escrow-budget@9c199db4 (2026-07-20)

This pass. Confirmed by source read at 9c199db4; make check was not re-run this pass.

Artifact: repowazdogz-droid/escrow-budget