What is a formal proof?

A short explanation for non-specialists

A formal proof is a program that a computer can check. It does not rely on human judgment: either the proof is accepted by the checker, or it is rejected. There is no middle ground.

Think of it this way: a regular test checks that a program works for a few examples. A formal proof checks that it works for every possible input.

A simple example

Suppose we write a function that inserts a number into a sorted list. We want to prove that the result is still sorted. Here is what that looks like in Lean 4:

def insert (x : Nat) : List Nat → List Nat
| [] => [x]
| h :: t =>
if x ≤ h then x :: h :: t
else h :: insert x t

This inserts a number into the right position. If the number is smaller than the head, it goes first. Otherwise, it recurses.

Now we state what we want to prove: that inserting into a sorted list produces a sorted list.

-- "For any number x and any sorted list l,
-- insert x l is also sorted."
theorem insert_sorted
(x : Nat) (l : List Nat)
(h : Sorted l) : Sorted (insert x l)

The theoremkeyword tells Lean: “I claim this is true, and here is my proof.” If the proof has any gap or error, Lean refuses to compile.

How does the checking work?

Lean has a small, well-audited kernel (about 5,000 lines of code) that accepts or rejects proofs. Every proof, no matter how complex, must pass through this kernel.

The kernel does not care how the proof was found. It could have been written by a human, generated by an AI, or produced by an automated solver. What matters is that each logical step is valid.

If the proof compiles, it is correct. If it doesn't, it isn't.

Tests vs. formal proofs

A testsays: “I tried inserting 3 into [1, 2, 4] and the result was sorted.”

A formal proofsays: “For every number and everysorted list, insertion preserves sorting.”

Why does this matter for smart contracts?

Smart contracts handle real money. A bug in the arithmetic of a DeFi protocol can drain millions. Tests catch some bugs, audits catch more, but neither can guarantee correctness for all possible states.

A formal proof can. It is a mathematical certificate that the property holds in every case, not just the ones the auditor thought to check.

See it in practice

Lido V3 Vault Solvency Guarantee . A formally verified property of a production smart contract.