Projects · Formal verification · Research prototype · PROVEN
escrow-budget
What this establishes
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.
What this does not establish
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.
Trusted base
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.
Method
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.
Result
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.
Negative controls. Four TLA+ controls (receiver-dup, volatile-received, lazy-debit, and a plain bad model) produce their counterexamples; removing the write-ahead debit or the durable dedup breaks the Lean proof.
Reproduce
make clean && make check- Toolchain
- Lean 4 leanprover/lean4:v4.32.0 (mathlib-free); TLA+ Tools v1.7.4; Python 3 with Hypothesis
- 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.
Independent reproduction
None known.
Prior art and positioning
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.