An explainer series on formally verifying DeFi in Lean

AI writes the proofs. Lean checks them.

For years, the honest answer to "should I formally verify this smart contract?" was "yes, but the effort puts most teams off." That trade-off has quietly collapsed: AI models can now write the proofs, and Lean checks them. This series is the practical playbook.

Explainers

Part 1
You Can Formally Verify Your Smart Contract Today. Here's How.

The basics on the simplest model: an ERC20-like token and an ERC4626-like vault.
Part 2
When the Proof Refuses, You're Looking at an Attack.

Round-trip loss bounds on the Part 1 vault. The unconditional loss bound doesn't hold; with the right side conditions, it does — and they read back as the inflation-attack threat model.

Case studies

Case study
Lending Market

A Lean 4 model of the Morpho Market core logic — supply and collateral pools, protocol actions, and machine-checked safety theorems covering healthy position preservation, solvency under explicit conditions, and lender value protection.

More explainers and case studies will follow as the series develops.