Tama

Tutorial

Your first contract

A guided walk from a fresh Tama project to a proved, compiled, tested, and audited ERC20Lite contract.

What we’re going to build

This tutorial starts from the contract Tama actually scaffolds today: ERC20Lite. It is a small token contract with an owner, balances, a total supply, transfers, ownership transfer, specifications, Lean proofs, generated Solidity bridge files, and Foundry mirror tests.

By the end you will have:

  • a fresh Tama project with a Verity contract,
  • machine-checked Lean proofs for the starter obligations,
  • Foundry fuzz tests and an invariant that mirror those obligations,
  • generated Yul, bytecode, ABI, manifests, and Solidity deployer files,
  • a green tama audit report you can attach to a release.

Step 1: Scaffold the project

tama init my-protocol
cd my-protocol

tama init creates a Foundry-shaped project and fills in a complete Verity starter:

my-protocol/
├── tama.toml
├── tama.lock
├── foundry.toml
├── lakefile.toml
├── lake-manifest.json
├── lean-toolchain
├── verity/
│   ├── src/
│   │   ├── MyProtocol.lean
│   │   └── MyProtocol/ERC20Lite.lean
│   ├── spec/MyProtocol/
│   │   ├── Spec.lean
│   │   └── Spec/ERC20LiteSpec.lean
│   └── proof/MyProtocol/
│       ├── Proof.lean
│       └── Proof/ERC20LiteProof.lean
├── src/generated/verity/
│   ├── ERC20LiteIface.sol
│   └── ERC20LiteDeployer.sol
├── test/verity/ERC20Lite.t.sol
├── script/ERC20Lite.s.sol
└── artifacts/

The generated project is intentionally complete. You can build it before you write any new contract, and every file in the starter participates in the proof, build, test, and audit loop. MyProtocol.lean, Spec.lean, and Proof.lean are aggregate modules: each one re-exports the per-contract files underneath it, so adding a new contract is a matter of writing the three sibling files and adding one import line to each aggregate.

Step 2: Check the local toolchain

tama doctor

doctor verifies the local CLI, Lean/Lake, Foundry, solc, Git, the project lockfile, and the resolved Verity revision. A healthy project prints checks like:

Checks:
  ok   tama            0.1.5
  ok   lean            4.22.0
  ok   lake            5.0.0-src+ba2cbbf (Lean version 4.22.0)
  ok   forge           1.6.0-v1.6.0-rc1
  ok   solc            0.8.33
  ok   git             2.43.0
  ok   lake buildDir   artifacts/lean
  ok   verity          requested <rev>, resolved <rev>
  ok   lock            current

If generated directories or lock inputs drift, run:

tama doctor --fix

--fix only applies safe repairs: it creates missing generated directories, repairs safe dependency drift where possible, and refreshes tama.lock. It does not rewrite your contract, spec, proof, or test sources.

Step 3: Read the implementation

Open verity/src/MyProtocol/ERC20Lite.lean. The starter uses the current Verity surface, which is Lean code that describes EVM storage and callable functions:

import Contracts.Common

namespace MyProtocol

open Verity hiding pure bind
open Contracts
open Verity.EVM.Uint256
open Verity.Stdlib.Math

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

Three details are worth noticing before moving on.

The storage slots are explicit. slot 0, slot 1, and slot 2 become part of the generated manifest and are checked by tama audit storage-layout.

Arithmetic is checked. safeAdd returns an optional value, and requireSomeUint turns overflow into a revert rather than a wrapped integer.

The self-transfer branch is deliberate. Without it, reading and writing the same mapping key twice can accidentally double-count a transfer to yourself.

Step 4: Read the specification

Open verity/spec/MyProtocol/Spec/ERC20LiteSpec.lean. This file is pure Lean: every top-level def is an obligation Tama tracks.

import MyProtocol.ERC20Lite

namespace MyProtocol.Spec.ERC20LiteSpec

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 balanceOf_spec (account : Address) (result : Uint256) (s : ContractState) : Prop :=
  result = s.storageMap 1 account

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

end MyProtocol.Spec.ERC20LiteSpec

The real starter contains eleven obligations. They cover frame conditions, read-only views, authorized effects, and unauthorized no-change behavior. Helpers belong outside this spec file, because Tama treats the spec module as the source of public proof obligations.

Open verity/proof/MyProtocol/Proof/ERC20LiteProof.lean. Proof theorems are ordinary Lean declarations — no Tama annotation is needed:

theorem balanceOf_returns_storage_balance (account : Address) (s : ContractState) :
  let result := ((balanceOf account).run s).fst
  balanceOf_spec account result s := by
  simp [balanceOf_spec, balanceOf, balancesSlot, Bind.bind, Pure.pure]

The generated file also contains larger state-transition proofs with case splits for mint, transfer, and transferOwnership. Tama discovers which obligation each theorem proves from the elaborated environment: a theorem discharges a spec when its conclusion — after stripping the data inputs — is that spec applied (or a positive conjunction containing it). balanceOf_returns_storage_balance concludes balanceOf_spec …, so it discharges balanceOf_spec.

Theorems whose conclusion is anything else are helper facts. They can make the proof easier to read, but they do not appear as release obligations.

Step 6: Check implementation and spec

tama check

check builds the implementation and spec targets, but it skips proof modules so the feedback loop stays fast:

Check scope:
  targets: MyProtocol, MyProtocol.Spec
  proofs: not run; use `tama build`

Steps:
  run  cache        prepare Lake package checkouts
  ok   cache        Lake packages ready
  run  lake         build MyProtocol and MyProtocol.Spec
  ok   lake         implementation/spec targets accepted
Check completed: MyProtocol and MyProtocol.Spec accepted

Use this command while editing implementation or spec files. Move to tama build when you need proof checking and generated artifacts.

Step 7: Build the proved bytecode

tama build

build runs the full path:

Build steps:
  run  proof-check     Lean elaborates implementations, specs, and proofs
  ok   proof-check     proof modules accepted by Lake
  run  verity-codegen  Verity emits Yul, ABI, storage, and trust reports
  ok   verity-codegen  compiler artifacts generated
  run  manifest        Tama adapts Verity outputs into contract manifests
  ok   manifest        1 manifest: ERC20Lite
  run  dischargers     Lean discovers proof dischargers by spec type
  ok   dischargers     dischargers resolved
  run  trust-probe     Lean validates dischargers and records proof dependencies
  ok   trust-probe     trust-boundary inputs written
  run  validate        ERC20Lite manifest schema and artifact paths
  ok   validate        ERC20Lite manifest validated
  run  solc            ERC20Lite Yul through solc standard JSON
  ok   solc            ERC20Lite bytecode and hash written
  run  bridge          ERC20Lite Solidity interface and deployer
  ok   bridge          ERC20Lite bridge files generated
  run  forge           Foundry compiles generated Solidity bridges and project tests
  ok   forge           forge build completed
Build completed: 1 manifest

After this finishes, generated files under src/generated/verity/ contain the actual interface and deployer for the compiled Verity bytecode. The manifest under artifacts/manifest/ERC20Lite.json records the source paths, ABI, selectors, storage layout, bytecode hash, obligations, mirrors, and trust inputs.

Step 8: Run the mirror tests

tama test

The starter has ten Foundry tests:

Ran 10 tests for test/verity/ERC20Lite.t.sol:ERC20LiteTest
[PASS] invariant_totalSupplyTracksMinted()
[PASS] testFuzzBalanceOfMirrorsGeneratedBytecode(address,uint256)
[PASS] testFuzzDeploymentSetsOwner(address)
[PASS] testFuzzMintRevertsForNonOwner(address,address,uint256)
[PASS] testFuzzMintUpdatesBalanceAndSupply(address,uint256)
[PASS] testFuzzTransferDebitAndCredit(address,uint256,uint256)
[PASS] testFuzzTransferOwnershipChangesOwner(address)
[PASS] testFuzzTransferOwnershipPreservesTokenState(address,address,uint256)
[PASS] testFuzzTransferOwnershipRevertsForNonOwner(address,address)
[PASS] testFuzzTransferPreservesTotalSupply(address,uint256,uint256)
Suite result: ok. 10 passed; 0 failed; 0 skipped

Open test/verity/ERC20Lite.t.sol and look for comments like:

// 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");
    require(token.totalSupply() == minted, "supply preserved");
}

// tama: mirrors=<spec> binds a Foundry fuzz test or invariant to the same spec definition a Lean theorem discharges. A spec is covered when Tama can see both sides: at least one Lean discharger and at least one executable mirror, unless the spec is explicitly listed as proof-only in tama.toml.

Step 9: Audit the release boundary

tama audit

The audit checks that the proof, generated artifacts, bytecode, mirrors, and trust boundary still agree:

Checks:
  ok   structure       Required files, generated paths, and bytecode hashes
  ok   selectors       ABI selectors/topics, Solidity declarations, and Yul dispatch
  ok   storage-layout  Storage slots, overlap, encodings, and compiler layout drift
  ok   coverage        Public obligations have Foundry mirrors or proof-only reasons
  ok   trust-boundary  Lean axioms, sorryAx, unresolved declarations, and trust reports

Audit passed: 5 checks, 1 contract, 0 issues

The trust-boundary check is the one to read carefully before a release. It walks proof dependencies for every theorem that discharges a spec and rejects sorry or unallowlisted axioms. The starter allowlist lives in tama.toml and is intentionally small.

Step 10: Inspect the artifacts

Use tama inspect to read one contract artifact at a time:

tama inspect ERC20Lite manifest
tama inspect ERC20Lite selectors
tama inspect ERC20Lite abi
tama inspect ERC20Lite storage-layout
tama inspect ERC20Lite obligations
tama inspect ERC20Lite mirrors
tama inspect ERC20Lite trust

Every inspector also supports JSON output:

tama --json inspect ERC20Lite manifest

These commands are useful in CI and release notes because they expose the same contract data the audit uses: selectors, ABI, storage slots, Yul and bytecode paths, obligations, Foundry mirrors, and trusted Lean assumptions.

Step 11: Deploy from the generated bridge

After tama build, the script in script/ERC20Lite.s.sol can deploy the generated bytecode:

forge script script/ERC20Lite.s.sol:DeployERC20Lite

Set ERC20LITE_OWNER to choose the initial owner:

ERC20LITE_OWNER=0x0000000000000000000000000000000000000001 \
  forge script script/ERC20Lite.s.sol:DeployERC20Lite

The script imports ERC20LiteDeployer, so it deploys the bytecode generated from the Verity source you just proved and audited.

Where to go next