Lean for Security Proofs, Part 2: Escrow Invariants in Practice

In Part 1 we focused on the mindset and workflow. Here we move to a more realistic system: a simple escrow processor with a pending payout queue and a maximum daily exposure limit.

The model is intentionally small, but it reflects how real payout systems are built. We track funds in three buckets and enforce a limit on pending payouts.

Model the state

We represent the escrow with three balances and a limit. The fields capture the minimum information needed to reason about safety.

structure EscrowState where
  treasury : Nat
  pending : Nat
  paid : Nat
  maxPending : Nat

def total (s : EscrowState) : Nat :=
  s.treasury + s.pending + s.paid

Define operations with explicit guards

We add two operations:

• request moves funds from treasury into pending, but only if there is enough treasury balance and the pending limit is not exceeded.
• settle moves funds from pending to paid, but only if the pending balance is large enough.

def request (s : EscrowState) (amount : Nat) : Option EscrowState :=
  if h1 : amount <= s.treasury then
    if h2 : s.pending + amount <= s.maxPending then
      some (EscrowState.mk (s.treasury - amount) (s.pending + amount) s.paid s.maxPending)
    else
      none
  else
    none

def settle (s : EscrowState) (amount : Nat) : Option EscrowState :=
  if h : amount <= s.pending then
    some (EscrowState.mk s.treasury (s.pending - amount) (s.paid + amount) s.maxPending)
  else
    none

Using Option makes the failure mode explicit. In a smart contract, these would map to reverts. In a service, they would map to a rejected request.

Invariant 1: conservation of value

A basic but critical invariant is conservation of value. No operation should create or destroy funds.

theorem request_some_of_bounds
  (s : EscrowState)
  (amount : Nat)
  (h1 : amount <= s.treasury)
  (h2 : s.pending + amount <= s.maxPending) :
  request s amount =
    some (EscrowState.mk (s.treasury - amount) (s.pending + amount) s.paid s.maxPending) := by
  simp [request, h1, h2]


theorem request_total_preserved
  (s : EscrowState)
  (amount : Nat)
  (h1 : amount <= s.treasury)
  (h2 : s.pending + amount <= s.maxPending) :
  total (EscrowState.mk (s.treasury - amount) (s.pending + amount) s.paid s.maxPending) =
    total s := by
  simp [total, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]


theorem settle_total_preserved
  (s : EscrowState)
  (amount : Nat)
  (h : amount <= s.pending) :
  total (EscrowState.mk s.treasury (s.pending - amount) (s.paid + amount) s.maxPending) =
    total s := by
  simp [total, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]

This is the property that prevents stealth leakage across accounting boundaries. If it is wrong, you can lose or mint value without noticing.

Invariant 2: pending exposure stays bounded

The pending limit is a real-world control used to cap exposure or rate limit payouts. Lean lets you prove that the request operation never violates it.

theorem request_pending_bound
  (s : EscrowState)
  (amount : Nat)
  (h1 : amount <= s.treasury)
  (h2 : s.pending + amount <= s.maxPending) :
  s.pending + amount <= s.maxPending := by
  exact h2

This example is simple on purpose. In larger systems, the bound lemma becomes more involved and is exactly the kind of thing a refactor can accidentally break.

From proofs to engineering checks

Once these properties exist, you can wire them into your engineering process:

• Use the Lean model as a reference spec and oracle for property tests.
• Fuzz the implementation and let the Lean model act as the oracle for valid sequences and expected post-state.
• Add runtime invariant checks for high-risk paths.

That combination makes it hard for a bug to survive. If code changes, the proof breaks and the fuzzer finds it.

Extend the model

To get closer to production, you can add:

• Authorization predicates for who can request or settle.
• Time-based limits and expiry for pending payouts.
• Fee schedules with explicit rounding rules.

The key is to grow the model only when a new invariant matters. Lean rewards small, clear steps.

Next up

Part 3 shows how to mirror these invariants in a minimal Rust system with property tests and runtime checks, so the proof stays enforced in code.

Ready to de-risk your stack?

We deliver formal specs, differential fuzzing suites, and conformance reports with remediation guidance.

• Book a Triage
• Request Scope