Lean 4 Formal verification EVM

Verity

Name: Verity
Author: LFG Labs

Write smart contracts in Lean. Compile to EVM. Prove them correct.

Pipeline: Spec → EDSL → IR → Yul
Surface: Storage, guards, events, typed externals
Assurance: Machine-checked claims, explicit assumptions

Side by side

The same contract, lifted into Lean.

Same shape as Solidity: guards, ABI, events, externals. All of it visible to proofs.

SolidityRuntime implementation surface

contract Escrow {
    address public owner;
    mapping(address => uint256) public balances;

    event Deposited(address indexed account, uint256 amount);
    event Withdrawn(address indexed account, uint256 amount);

    modifier onlyOwner() {
        require(msg.sender == owner, "UNAUTHORIZED");
        _;
    }

    function deposit() external payable {
        balances[msg.sender] += msg.value;
        emit Deposited(msg.sender, msg.value);
    }

    function withdraw(uint256 amount) external onlyOwner {
        require(amount <= balances[msg.sender], "INSUFFICIENT_BALANCE");
        bool ok = auditHook(msg.sender, amount);
        require(ok, "AUDIT_REJECTED");
        balances[msg.sender] -= amount;
        emit Withdrawn(msg.sender, amount);
    }
}

verity_contract Escrow where
  storage
    owner : Address := slot 0
    balances : Address -> Uint256 := slot 1

  event_defs
    Deposited(Address, Uint256)
    Withdrawn(Address, Uint256)

  linked_externals
    external auditHook(Address, Uint256) -> (Bool)

  modifier onlyOwner := do
    let sender <- msgSender
    let currentOwner <- getStorageAddr owner
    requireError (sender == currentOwner) Unauthorized()

  function deposit () : Unit := do
    let sender <- msgSender
    let amount <- msgValue
    let current <- getMapping balances sender
    let next <- requireSomeUint (safeAdd current amount) BalanceOverflow()
    setMapping balances sender next
    emit "Deposited" [sender.toNat, amount.toNat]

  function withdraw (amount : Uint256) with onlyOwner : Unit := do
    let sender <- msgSender
    let current <- getMapping balances sender
    requireError (amount <= current) InsufficientBalance()
    let ok <- externalCall auditHook [sender, amount]
    requireError ok AuditRejected()
    setMapping balances sender (current - amount)
    emit "Withdrawn" [sender.toNat, amount.toNat]

Modifiers: Plain verified helpers, no compiler magic.
External calls: Typed at the boundary; oracle assumptions are explicit.
Storage & events: Visible to specs, proofs, and compiler reports.

Start here

The Three-Layer Structure

Every contract is three things at once: a specification of what it should do, an implementation that runs, and a proof that ties them together.

Specification · what should be true


def mint_spec (to : Address) (amount : Uint256) (s s' : ContractState) : Prop :=
  s'.storageMap 1 to = add (s.storageMap 1 to) amount ∧
  s'.storage 2 = add (s.storage 2) amount ∧
  storageMapUnchangedExceptKeyAtSlot 1 to s s' ∧
  sameContext s s'

Implementation · what runs on chain


def mint (to : Address) (amount : Uint256) : Contract Unit := do
  onlyOwner
  let currentBalance ← getMapping balances to
  let newBalance ← requireSomeUint (safeAdd currentBalance amount) "Balance overflow"
  let currentSupply ← getStorage totalSupply
  let newSupply ← requireSomeUint (safeAdd currentSupply amount) "Supply overflow"
  setMapping balances to newBalance
  setStorage totalSupply newSupply

Proof · they agree


theorem mint_meets_spec (s : ContractState) (to : Address) (amount : Uint256)
  (h_owner : s.sender = s.storageAddr 0) :
  let s' := ((mint to amount).run s).snd
  mint_spec to amount s s' := by
  simp only [mint, onlyOwner, getMapping, setMapping]
  simp [h_owner]

Lean checks every proof at compile time. A broken proof is a broken build.