What is a formal proof?

A short explanation for non-specialists

A formal proof is a program that a computer can check. Either the proof is accepted, or it is rejected. There is no middle ground.

A test checks that code works for a few examples. A formal proof checks that it works for every possible input.

A concrete example

Consider a simplified ERC-20 token. The contract stores balances and a total supply. Here is the transfer function written in Verity, a framework for formally verified smart contracts:

-- Contract storage

verity_contract ERC20 where

storage

totalSupplySlot : Uint256 := slot 1

balancesSlot : Address → Uint256 := slot 2

-- Transfer tokens from sender to recipient

function transfer (to : Address, amount : Uint256) : Unit := do

let sender ← msgSender

let senderBalance ← getMapping balancesSlot sender

require (senderBalance >= amount) "Insufficient balance"

setMapping balancesSlot sender (sub senderBalance amount)

let recipientBalance ← getMapping balancesSlot to

setMapping balancesSlot to (add recipientBalance amount)

This reads like pseudocode, but it compiles to real EVM bytecode. Now we state a property we want to guarantee:

“Calling transfer never changes the total supply.”

-- The sum of all balances equals total supply

def supply_matches_balances (s : ContractState) : Prop :=

totalBalance s = s.storage 1

-- Transfer preserves the sum of all balances

def transfer_preserves_total (s s' : ContractState) : Prop :=

totalBalance s' = totalBalance s

And we prove it:

theorem transfer_preserves_totalSupply

(s : ContractState) (to : Address) (amount : Uint256)

(h_balance : s.storageMap 2 s.sender ≥ amount)

: transfer_preserves_total s (transfer to amount).runState s := by

-- transfer only touches balances (slot 2)

have h_slot : transfer does not write to slot 1

-- subtracting from sender and adding to recipient cancels out

have h_sum : sub a x + add b x = a + b

-- therefore total balance is unchanged, and so is total supply

exact eq.trans h_sum h_slot

The theorem keyword tells Lean: “I claim this is true, and here is my proof.” The by block contains the actual proof steps. If any step has a gap or error, Lean refuses to compile.

How does the checking work?

Lean has a small, well-audited kernel that accepts or rejects proofs. Every proof must pass through this kernel. It does not care how the proof was found: by a human, an AI, or an automated solver. What matters is that each step is valid.

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

Tests vs. formal proofs

A test says: “I transferred 50 tokens from Alice to Bob and the total supply didn't change.”

A formal proof says: “For every sender, every recipient, and every amount, transfer preserves total supply.”

Why does this matter for smart contracts?

Smart contracts handle real money. A bug in token arithmetic 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.

More research

Verity Verified Compiler

A Formally Verified Smart Contract Compiler in Lean 4.

Publication

Verity Benchmark

A benchmark suite for AI-driven formal proof generation on real smart contracts.

Publication

Lido V3 Vault Solvency Guarantee

A formally verified property of a production smart contract.

Case study