What’s in the box

tama init my-protocol scaffolds a Foundry project plus the Verity layers, populated with a working contract called ERC20Lite. It’s small enough to read in one sitting, and it exercises every part of Tama: storage, mappings, a constructor, multiple obligations, mirror tests, and a Foundry invariant that runs against generated bytecode.

The four files worth reading:

verity/src/MyProtocol/ERC20Lite.lean               # implementation
verity/spec/MyProtocol/Spec/ERC20LiteSpec.lean     # specification
verity/proof/MyProtocol/Proof/ERC20LiteProof.lean  # proofs
test/verity/ERC20Lite.t.sol                        # Foundry mirror tests

This page walks them in that order. The full source is in your project after tama init; what’s reproduced here are the parts worth pointing at.

The implementation

verity/src/MyProtocol/ERC20Lite.lean:

import Contracts.Common

namespace MyProtocol

verity_contract ERC20Lite where
  storage
    ownerSlot       : Address           := slot 0
    balancesSlot    : Address → Uint256 := slot 1
    totalSupplySlot : Uint256           := slot 2

  constructor (initialOwner : Address) := do
    setStorageAddr ownerSlot initialOwner
    setStorage totalSupplySlot 0

  function mint (toAddr : Address, amount : Uint256) : Bool := do
    let sender ← msgSender
    let currentOwner ← getStorageAddr ownerSlot
    require (sender == currentOwner) "Caller is not the owner"
    let currentBalance ← getMapping balancesSlot toAddr
    let newBalance ← requireSomeUint (safeAdd currentBalance amount) "Balance overflow"
    let currentSupply ← getStorage totalSupplySlot
    let newSupply ← requireSomeUint (safeAdd currentSupply amount) "Supply overflow"
    setMapping balancesSlot toAddr newBalance
    setStorage totalSupplySlot newSupply
    return true

  function transfer (toAddr : Address, amount : Uint256) : Bool := do
    let sender ← msgSender
    let senderBalance ← getMapping balancesSlot sender
    require (senderBalance >= amount) "Insufficient balance"
    if sender == toAddr then
      pure ()
    else
      let recipientBalance ← getMapping balancesSlot toAddr
      let newRecipientBalance ← requireSomeUint (safeAdd recipientBalance amount) "Recipient balance overflow"
      setMapping balancesSlot sender (sub senderBalance amount)
      setMapping balancesSlot toAddr newRecipientBalance
    return true

  function transferOwnership (newOwner : Address) : Unit := do
    let sender ← msgSender
    let currentOwner ← getStorageAddr ownerSlot
    require (sender == currentOwner) "Caller is not the owner"
    setStorageAddr ownerSlot newOwner

  function view balanceOf  (addr : Address) : Uint256 := ...
  function view totalSupply ()              : Uint256 := ...
  function view owner       ()              : Address := ...

end MyProtocol

A few things to notice.

Storage slots are explicit. slot 0, slot 1, slot 2 aren’t decoration — they’re the actual EVM storage slots. The generated manifest records them so tama audit storage-layout can compare what Lean expects with what the compiler emits.

safeAdd returns Option, not a wrapping sum. requireSomeUint turns a none into a revert. Overflow is a first-class concept the proof has to reason about, not a footnote.

transfer has a self-transfer branch. Naively reading balances[from] and writing balances[from] and balances[to] separately would double-count when from == to. The branch handles that case explicitly — partly for correctness, partly because the proof has to walk through both halves of the if.

transferOwnership is the access-control half of mint. mint guards behind sender == owner; transferOwnership guards behind the same predicate and rotates that owner to a successor. The pair gives the spec file two access-control obligations to demonstrate (one for each function, with both halves — authorized and unauthorized).

The specification

verity/spec/MyProtocol/Spec/ERC20LiteSpec.lean is pure Lean — no -- tama: comments anywhere. Every top-level def (and every #gen_spec invocation) in this file is automatically an obligation Tama tracks. Helpers, if any, must live outside the spec module:

import MyProtocol.ERC20Lite

namespace MyProtocol.Spec.ERC20LiteSpec

-- Frame conditions: parts of state the function never touches.
def transfer_total_supply_preserved (s s' : ContractState) : Prop :=
  s'.storage 2 = s.storage 2

def mint_owner_preserved (s s' : ContractState) : Prop :=
  s'.storageAddr 0 = s.storageAddr 0

def transferOwnership_supply_preserved (s s' : ContractState) : Prop :=
  s'.storage 2 = s.storage 2

def transferOwnership_balances_preserved
    (account : Address) (s s' : ContractState) : Prop :=
  s'.storageMap 1 account = s.storageMap 1 account

-- Read-only views: pure reads of storage.
def balanceOf_spec (account : Address) (result : Uint256) (s : ContractState) : Prop :=
  result = s.storageMap 1 account

def totalSupply_spec (result : Uint256) (s : ContractState) : Prop :=
  result = s.storage 2

def owner_spec (result : Address) (s : ContractState) : Prop :=
  result = s.storageAddr 0

-- Authorized-path effects: what an authorized caller observes.
def transferOwnership_authorized_sets_owner
    (newOwner : Address) (s s' : ContractState) : Prop :=
  s.sender = s.storageAddr 0 → s'.storageAddr 0 = newOwner

def transfer_balances_effect
    (toAddr : Address) (amount : Uint256) (s s' : ContractState) : Prop :=
  amount.val ≤ (s.storageMap 1 s.sender).val →
    (s.sender = toAddr →
      s'.storageMap 1 s.sender = s.storageMap 1 s.sender) ∧
    (s.sender ≠ toAddr →
      (s.storageMap 1 toAddr).val + amount.val ≤ Verity.Stdlib.Math.MAX_UINT256 →
        s'.storageMap 1 s.sender = (s.storageMap 1 s.sender) - amount ∧
        s'.storageMap 1 toAddr = (s.storageMap 1 toAddr) + amount)

-- Negative access control: unauthorized callers leave state alone.
def mint_unauthorized_no_change
    (toAddr : Address) (_amount : Uint256) (s s' : ContractState) : Prop :=
  s.sender ≠ s.storageAddr 0 →
    s'.storage 2 = s.storage 2 ∧
    s'.storageMap 1 toAddr = s.storageMap 1 toAddr

def transferOwnership_unauthorized_owner_unchanged
    (s s' : ContractState) : Prop :=
  s.sender ≠ s.storageAddr 0 → s'.storageAddr 0 = s.storageAddr 0

end MyProtocol.Spec.ERC20LiteSpec

The set is grouped to show the four common shapes a starter should exercise:

  1. Frame conditions — transfer_total_supply_preserved, mint_owner_preserved, transferOwnership_supply_preserved, transferOwnership_balances_preserved. The function does not touch that part of state. transfer_total_supply_preserved is also the contract’s conservation law: a token moves, nothing is created or destroyed.
  2. Read-only views — balanceOf_spec, totalSupply_spec, owner_spec. The query is a faithful read.
  3. Authorized-path effects — transferOwnership_authorized_sets_owner pins down what the owner observes after a successful rotation; transfer_balances_effect pins down the exact debit and credit on the success path, and demands the self-transfer branch leaves the entire balance mapping untouched — the well-known double-debit footgun gets a first-class proof obligation, not a comment.
  4. Negative access control — mint_unauthorized_no_change, transferOwnership_unauthorized_owner_unchanged. The complementary half of access control: not only does the authorized path do the right thing, the unauthorized path does nothing. This is the property that prevents a non-owner from minting tokens or stealing the contract.

Three are facts about pure reads. The rest are facts about state transitions — split between “what changes” (effects) and “what doesn’t change” (frames and revert-on-unauthorized).

The proofs

verity/proof/MyProtocol/Proof/ERC20LiteProof.lean discharges each spec definition. The transfer-supply proof is the most case-splitty:

import MyProtocol.Spec.ERC20LiteSpec
import Verity.Proofs.Stdlib.Automation

namespace MyProtocol.Proof.ERC20LiteProof

open Verity
open Verity.EVM.Uint256
open MyProtocol.Spec.ERC20LiteSpec
open MyProtocol.ERC20Lite

-- tama: discharges=transfer_total_supply_preserved
theorem transfer_total_supply_preserved_after_run
    (toAddr : Address) (amount : Uint256) (s : ContractState) :
    let s' := ((transfer toAddr amount).run s).snd
    transfer_total_supply_preserved s s' := by
  unfold transfer_total_supply_preserved
  by_cases h_balance : amount.val ≤ (s.storageMap 1 s.sender).val
  · simp [transfer, balancesSlot, msgSender, getMapping, ...,
          h_balance]
    by_cases h_same : s.sender = toAddr
    · simp [h_same, Verity.pure]
    · by_cases h_overflow : ... <;>
        simp [h_same, h_overflow, ...]
  · simp [transfer, ..., h_balance]

Two case splits drive that proof: did the sender have enough balance? and is the recipient the same as the sender? That’s a proof shape worth recognizing — one branch per require, one branch per non-trivial if. The simp invocations unfold the contract definitions and rely on the Verity standard library for the storage and arithmetic lemmas.

The implication-shaped specs (effects and negative access control) take a slightly different shape. They drop the let s' := ... binder because intro would otherwise consume it before reaching the implication’s antecedent, and they intro the precondition before discharging the conjunction:

-- tama: discharges=transferOwnership_authorized_sets_owner
theorem transferOwnership_authorized_sets_owner_after_run
    (newOwner : Address) (s : ContractState) :
    transferOwnership_authorized_sets_owner newOwner s
      ((transferOwnership newOwner).run s).snd := by
  unfold transferOwnership_authorized_sets_owner
  intro h_owner
  simp [transferOwnership, ownerSlot, msgSender, getStorageAddr,
    setStorageAddr, Contract.run, ContractResult.snd, Verity.bind,
    Bind.bind, Verity.require, h_owner]

The transfer_balances_effect proof is the most elaborate of the new ones: it case-splits on s.sender = toAddr to handle the spec’s two branches separately, uses subst in the self-transfer branch so the balance precondition lines up after the substitution, and ends with a show step that rewrites the s' - amount form into the sub s' form setMapping literally produces. (The two are definitionally equal via the HSub instance, but simp’s add_comm fires on + while leaving sub alone, so the sender side has to be canonicalized by hand.)

The model is symmetric. The spec file declares an obligation by defining transfer_total_supply_preserved; the proof claims it with -- tama: discharges=transfer_total_supply_preserved directly above the theorem, and Lean checks that the theorem target is that spec application; the Foundry test mirrors it with a matching // tama: mirrors=transfer_total_supply_preserved (next section). Theorems and lemmas without a discharges= tag are silently treated as helpers; the ten other obligations each carry their own discharges= tag pointing at the matching spec def, and each spec is mirrored by at least one testFuzz_* (or invariant_*) function in the Foundry test file.

The mirror tests

test/verity/ERC20Lite.t.sol does three things.

One. Property-shaped fuzz tests. Each obligation has a testFuzz_* function that exercises the same property on the real bytecode, with a // tama: mirrors=<spec> comment directly above:

// tama: mirrors=transfer_total_supply_preserved
function testFuzzTransferPreservesTotalSupply(
    address recipient, uint256 rawMint, uint256 rawTransfer
) public {
    ERC20LiteIface token = deployToken();
    uint256 minted = rawMint % 1e36;
    uint256 amount = minted == 0 ? 0 : rawTransfer % (minted + 1);
    require(token.mint(address(this), minted), "mint");
    require(token.transfer(recipient, amount), "transfer");
    // ... balance assertions ...
    require(token.totalSupply() == minted, "supply preserved");
}

The proof says for all states and inputs, total supply is preserved. The fuzz test exercises the same property on bytecode generated from the same source, under thousands of random schedules. If the proof and the deployed bytecode are about the same contract, they agree. If a bridge regeneration drifts, the fuzz test catches it before audit even runs.

Two. Negative access-control tests with vm.prank / vm.expectRevert. The unauthorized-path specs are mirrored by tests that impersonate a non-owner and assert the call reverts and the slot is untouched:

// tama: mirrors=transferOwnership_unauthorized_owner_unchanged
function testFuzzTransferOwnershipRevertsForNonOwner(
    address attacker, address newOwner
) public {
    vm.assume(attacker != address(this));
    ERC20LiteIface token = deployToken();
    address ownerBefore = token.owner();
    vm.prank(attacker);
    vm.expectRevert();
    token.transferOwnership(newOwner);
    require(token.owner() == ownerBefore, "owner unchanged");
}

Two pieces of state are checked: the call reverts (via expectRevert), and the storage slot is unchanged after the revert. A would-be exploit that bypassed the require would either not revert (caught by expectRevert) or modify state across the revert (caught by the post-call read).

Three. A Foundry stateful invariant. A handler calls mint and transfer with random parameters across a long stateful run, while invariant_totalSupplyTracksMinted checks the global property at every step:

// tama: mirrors=transfer_total_supply_preserved
function invariant_totalSupplyTracksMinted() public view {
    require(invariantToken.totalSupply() == invariantMinted, "invariant supply");
}

function handlerMint(uint8 accountIndex, uint256 rawAmount) public {
    uint256 amount = rawAmount % 1e24;
    require(invariantToken.mint(invariantAccount(accountIndex), amount), "invariant mint");
    invariantMinted += amount;
}

This is the standard Foundry invariant pattern. The proof anchors the property; the invariant exercises it under stateful fuzzing. Tama treats one spec being mirrored by both a fuzz test and a Foundry invariant as the normal case — mirrors=<spec> may appear above any number of testFuzz*/invariant_* functions, and a single test may mirror several specs (mirrors=foo,bar, no whitespace after commas). Helper functions like handlerMint carry no mirrors= tag and are not tracked.

Build and audit

tama build
tama audit

You should see eleven obligations covered:

audit:
  ✓ structure       artifacts present, hashes match
  ✓ selectors       6 functions agree across Verity / manifest / Yul / Solidity
  ✓ storage-layout  3 slots, no overlap
  ✓ coverage        every spec has a discharger and a mirror
  ✓ trust-boundary  no sorry, axioms allowlisted

Six functions, three storage slots, eleven obligations all mirrored. The whole pipeline you just toured is sealed end-to-end.

Where to go next