Lean for Security Proofs, Part 3: Enforcing the Proof in Rust

Part 2 gave us an escrow model with proofs for conservation and exposure limits. Part 3 shows how to enforce those same invariants in a minimal Rust system, without pretending the proof automatically covers the implementation.

The approach is simple: keep a tiny, explicit model in Lean, then mirror the core invariants in Rust with property tests and runtime checks. The proof is the specification. The Rust code is the reality.

The minimal architecture

We want the Rust system to map cleanly to the Lean model:

• The state has treasury, pending, paid, and a pending limit.
• Operations are request and settle, with explicit guards.
• Invariants are checked after every successful state change.

This keeps the mapping tight and reduces the risk of drift.

Rust state and operations

Below is a minimal Rust implementation of the escrow operations. The code returns Option to mirror the Lean failure mode. In production you might use Result with richer errors.

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct EscrowState {
    pub treasury: u128,
    pub pending: u128,
    pub paid: u128,
    pub max_pending: u128,
}

impl EscrowState {
    pub fn total(self) -> u128 {
        self.treasury + self.pending + self.paid
    }

    pub fn request(self, amount: u128) -> Option<Self> {
        if amount > self.treasury {
            return None;
        }
        if self.pending + amount > self.max_pending {
            return None;
        }
        let next = Self {
            treasury: self.treasury - amount,
            pending: self.pending + amount,
            paid: self.paid,
            max_pending: self.max_pending,
        };
        debug_assert!(next.total() == self.total());
        Some(next)
    }

    pub fn settle(self, amount: u128) -> Option<Self> {
        if amount > self.pending {
            return None;
        }
        let next = Self {
            treasury: self.treasury,
            pending: self.pending - amount,
            paid: self.paid + amount,
            max_pending: self.max_pending,
        };
        debug_assert!(next.total() == self.total());
        Some(next)
    }
}

Notice the invariant check is local and explicit. That is the Rust analogue of our Lean proofs: every operation must preserve conservation of value.

Property tests that mirror the proof

Next we enforce the invariants under randomized inputs. The property test asserts that any successful request or settle preserves total value and maintains the pending bound.

#[cfg(test)]
mod tests {
    use super::EscrowState;
    use proptest::prelude::*;

    fn sample_state() -> impl Strategy<Value = EscrowState> {
        (0u128..1_000_000, 0u128..1_000_000, 0u128..1_000_000, 1u128..2_000_000)
            .prop_map(|(treasury, pending, paid, max_pending)| EscrowState {
                treasury,
                pending,
                paid,
                max_pending: max_pending.max(pending),
            })
    }

    proptest! {
        #[test]
        fn request_preserves_total(state in sample_state(), amount in 0u128..1_000_000) {
            if let Some(next) = state.request(amount) {
                prop_assert_eq!(next.total(), state.total());
                prop_assert!(next.pending <= next.max_pending);
            }
        }

        #[test]
        fn settle_preserves_total(state in sample_state(), amount in 0u128..1_000_000) {
            if let Some(next) = state.settle(amount) {
                prop_assert_eq!(next.total(), state.total());
            }
        }
    }
}

These are not formal proofs, but they enforce the same properties on the implementation. If the Rust code drifts from the Lean model, the tests fail.

Fuzzing and property tests with Lean as the oracle

Once the Lean model is stable, you can use it as the oracle for fuzzing. The core idea is simple:

1. Generate randomized sequences of operations.
2. Execute them against the Rust implementation.
3. Execute them against the Lean model (or a distilled reference).
4. Assert the post-state and invariants match.

This gives you a high-signal fuzz suite because the model defines what is allowed. When the implementation diverges, you get a minimized, replayable counterexample that points directly at the invariant break.

The same oracle also powers property tests. You can shrink the input space to targeted properties (like conservation of value) while still grading the results against the Lean model.

Keeping the Lean and Rust models aligned

The biggest risk is drift. To prevent it:

• Keep the Lean model minimal and focused on invariants.
• Use the Lean model as the authoritative spec in code review.
• Add a mapping document that states how each Lean operation maps to Rust.
• Make property tests the contract: no merge if they fail.

The ideal workflow is short and repeatable: update Lean model, update Rust, update tests, then rerun proofs and fuzzing.

A production-safe feedback loop

In real systems we add two more layers:

• Fuzz the Rust operations with adversarial sequences of requests and settles. Use the Lean model as the oracle that grades each sequence.
• Add runtime invariant checks on critical code paths for defense in depth.

Formal proofs reduce the unknowns. Fuzzing and runtime checks reduce the unknown unknowns. Together they form a practical, high-assurance loop.

The takeaway

Lean gives you mathematical confidence. Rust gives you operational reality. The bridge is explicit invariants, enforced in code and tests. That is how proofs survive contact with production.

Ready to de-risk your stack?

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

• Book a Triage
• Request Scope