PROVEN
Finding · authorise
A spending cap was proved to hold in every state the system can reach, not just the ones anyone tested.
§ 1
The record
FINDING · budget-bound-for-all-reachable-statesauthorise
A spending cap was proved to hold in every state the system can reach, not just the ones anyone tested.
- Claim
- 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.
- Status
- PROVEN Follows from stated premises inside a named frame.
- Subject
- A Lean 4 model of the escrow protocol (model). built for the study
- Frame
- Any finite set of replicas, any non-negative amounts; crash is global in the Lean model.
- Method
- Induction over reachable states with the budget bound as the invariant; a TLA+ model and a Python fault harness exercise what the proof does not.
- Oracle
- The Lean 4 kernel (v4.32.0), axioms propext and Quot.sound only.
- Negative control
- Present Four proved negative controls: remove a guard and the theorem must fail.
- Limitation
- 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.
- Source
- repowazdogz-droid/escrow-budget @ 9c199db4
- Reproduce
make clean && make check
- Independent reproduction
- None known.
§ 2
Where this sits
This finding answers Individually compliant is not collectively safe and supports the AUTHORISE stage of the operating method.