Lean for Security Proofs, Part 1: A Practical Starting Point

Lean is a proof assistant that lets you express system models and security claims as executable, checkable mathematics. It is not a replacement for engineering discipline, but it is the best way to make assumptions explicit and to prove properties that are easy to hand-wave.

This series focuses on using Lean 4 for practical security work. The goal is not to formalize everything, but to prove the properties that would hurt the most if they were wrong.

Where Lean fits in a security workflow

Lean is strongest when the property is crisp and the failure is expensive. For security work, that usually means:

• Accounting and conservation of value.
• Authorization checks and state transition rules.
• Protocol invariants like ordering, freshness, or uniqueness.
• Equivalence between reference and optimized implementations.

Lean gives you a proof that the invariant holds for every valid execution. That is a different class of confidence than tests alone.

Pick a boundary worth proving

Proofs scale poorly if the boundary is wrong. The best starting points are small, high-value units:

• A critical function with non-trivial branching logic.
• A state machine with clear allowed and forbidden transitions.
• A contract module that must preserve a conservation law.

If you pick a boundary that is too large, you will spend all your time modeling things that are not essential to the property you care about.

Model the system, not the implementation

Proofs should model the behavior, not the code. Build a minimal state model that captures the actual security risk and ignore everything else.

For example, you can remove networking, persistence, or analytics and still prove a conservation property. That minimal model is often enough to reveal missing invariants and hidden assumptions.

Turn assumptions into invariants

Every security review starts with implicit claims. Make them explicit in Lean:

• “Balances always add up” becomes a total preservation lemma.
• “Only authorized withdrawals” becomes a predicate and a proof about it.
• “No replay” becomes a uniqueness property on nonces or message ids.

A good invariant is a total function from state to Prop. Once it exists, you can prove that each operation preserves it.

A practical proof workflow

A reliable workflow for Lean proofs looks like this:

1. Define a minimal state and a handful of operations.
2. Write the invariant as a function or predicate.
3. Prove per-operation preservation lemmas with simp and small arithmetic reasoning.
4. Add composition theorems if operations are chained or sequenced.

This keeps proofs local and resilient to code evolution.

Combine with fuzzing and property testing

Lean does not replace tests. It gives you a formal oracle that tests can use. If the proof says an invariant must hold, use property tests and fuzzing to look for violations in the implementation. The formal model becomes the specification the engineering system must satisfy.

The high-leverage path is to prove one or two invariants in Lean, then turn those into fuzzing or property tests that run continuously. Treat the Lean model as your oracle: the fuzzer and property tests generate sequences, and the oracle decides whether the implementation drifted from the proof.

Common pitfalls

Teams tend to get stuck when they:

• Model too much and lose the thread of the property.
• Skip adversary modeling and assume honest behavior.
• Prove the wrong property because the invariant is underspecified.

If the proof is long, it is often a sign the model is bloated or the property is unclear.

Getting started

Begin with a single module and a single invariant. The goal is not to formalize an entire codebase, but to identify the smallest model that captures your security argument. Once that is stable, extend the model in small steps.

Next up

Part 2 walks through a more realistic escrow-style system with a pending payout queue, a limit on daily exposure, and proofs for the key invariants.

Ready to de-risk your stack?

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

• Book a Triage
• Request Scope