Your first contract

What we’re going to build

A TipJar contract: people send ETH, the contract records who paid in and how much, and only those people can withdraw what they put in. The property we want to prove is the obvious one and the one every real exploit violates:

The sum of recorded balances is exactly the amount of ETH the contract holds. Nothing is created. Nothing disappears.

By the end of this tutorial you will have:

• a working Tama project with the TipJar contract,
• a Lean proof of that invariant, machine-checked,
• a Foundry mirror test that exercises the same property as a fuzz test,
• a green tama audit report you could attach to a release.

Step 1 — Scaffold a project

tama init tipjar-protocol
cd tipjar-protocol

tama init writes a Foundry-shaped project plus the Verity layers:

tipjar-protocol/
├── tama.toml          # project marker, Verity pin, audit policy
├── tama.lock          # resolved versions
├── foundry.toml       # standard Foundry config
├── lakefile.toml      # Lake build config (yours to edit)
├── lean-toolchain     # pinned Lean version
├── verity/
│   ├── src/           # Verity contracts
│   ├── spec/          # specifications and invariants
│   └── proof/         # machine-checked proofs
├── src/generated/     # generated Solidity bridges (do not edit)
├── test/verity/       # Foundry mirror tests
└── artifacts/         # build outputs

The starter ships with a real ERC20Lite example that already builds and audits. Reading the starter walks through it line-by-line if you want to see a finished Verity contract before writing your own; otherwise, verify your toolchain by running:

tama doctor
tama check

tama check runs the fast Lean elaboration of implementation + spec — proofs come later in tama build. This should finish in seconds.

Step 2 — Add the TipJar

tama new TipJar

This creates four files:

verity/src/TipjarProtocol/TipJar.lean               # implementation
verity/spec/TipjarProtocol/Spec/TipJarSpec.lean     # specification
verity/proof/TipjarProtocol/Proof/TipJarProof.lean  # proof
test/verity/TipJar.t.sol                            # Foundry mirror test

Open verity/src/TipjarProtocol/TipJar.lean and replace the scaffold body with:

import Verity

namespace TipjarProtocol

verity_contract TipJar where

  storage
    balances : mapping(address, uint256)
    total    : uint256

  function deposit() external payable do
    let me  := msg.sender
    let amt := msg.value
    balances[me] := balances[me] + amt
    total        := total + amt

  function withdraw(amount : uint256) external do
    let me := msg.sender
    require balances[me] >= amount
    balances[me] := balances[me] - amount
    total        := total - amount
    transfer me amount

end TipjarProtocol

This is the entire implementation. It looks like Solidity because that’s the register Verity reaches for — storage, function, require, transfer. Underneath, every line is an expression in a Lean type theory that the compiler can reason about.

Step 3 — Write the specification

Open verity/spec/TipjarProtocol/Spec/TipJarSpec.lean and replace its body with:

import TipjarProtocol.TipJar

namespace TipjarProtocol.Spec.TipJarSpec

/-- The recorded `total` is always the sum of every balance. -/
def total_tracks_balances (s : TipJar.State) : Prop :=
  s.total = s.balances.sumValues

end TipjarProtocol.Spec.TipJarSpec

One statement: an invariant — a property the contract must preserve through every call. Postconditions for individual functions (e.g. “after deposit, total grows by exactly msg.value”) would be additional top-level defs in the same file; we’ll keep this tutorial focused on the invariant.

The spec file is pure Lean. There are no -- tama: comments — every top-level def (and every #gen_spec invocation) is automatically an obligation Tama tracks. Helpers like auxiliary lemmas or scratch defs must live outside the spec file; the build rejects anything other than import, namespace, open, def, #gen_spec, and end here. The proof file (next step) is where each obligation gets discharged, and a Foundry test (step 5) is where each one gets mirrored.

Step 4 — Discharge the proofs

Open verity/proof/TipjarProtocol/Proof/TipJarProof.lean:

import TipjarProtocol.Spec.TipJarSpec

namespace TipjarProtocol.Proof.TipJarProof

open TipjarProtocol.Spec.TipJarSpec
open TipjarProtocol.TipJar

-- tama: discharges=total_tracks_balances
theorem deposit_preserves_invariant
    (pre : TipJar.State) (call : TipJar.Call)
    (h : TipJarSpec.total_tracks_balances pre) :
    TipJarSpec.total_tracks_balances (TipJar.deposit pre call) := by
  simp [TipJarSpec.total_tracks_balances, TipJar.deposit,
        Mapping.sumValues_update_add]

-- tama: discharges=total_tracks_balances
theorem withdraw_preserves_invariant
    (pre : TipJar.State) (amount : UInt256)
    (h : TipJarSpec.total_tracks_balances pre)
    (k : pre.balances[msg.sender] ≥ amount) :
    TipJarSpec.total_tracks_balances (TipJar.withdraw pre amount) := by
  simp [TipJarSpec.total_tracks_balances, TipJar.withdraw,
        Mapping.sumValues_update_sub k]

end TipjarProtocol.Proof.TipJarProof

Each theorem says: if the invariant holds before the call, it holds after the call. The by simp [...] is the proof — Lean’s simplifier unfolds the definitions and the lemmas listed, and Verity’s standard library takes care of the mapping arithmetic. Verity’s debugging-proofs guide catalogues the tactics and error messages you’ll meet most often.

Each -- tama: discharges=<spec> comment claims a spec definition from TipjarProtocol/Spec/TipJarSpec.lean. Two theorems can discharge the same spec (as above), one theorem can discharge several (discharges=foo,bar), and any theorem or lemma without a discharges= tag is silently treated as a helper and never appears in the manifest.

Step 5 — Write the mirror test

Open test/verity/TipJar.t.sol and replace the body:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

import {Test} from "forge-std/Test.sol";
import {TipJarIface} from "src/generated/verity/TipJarIface.sol";
import {TipJarDeployer} from "src/generated/verity/TipJarDeployer.sol";

contract TipJarTest is Test {
    TipJarIface jar;

    function setUp() public {
        jar = TipJarDeployer.deploy();
    }

    // tama: mirrors=total_tracks_balances
    function invariant_totalTracksBalances() public view {
        assertEq(address(jar).balance, jar.total());
    }

    // tama: mirrors=total_tracks_balances
    function testFuzz_deposit(address who, uint96 amount) public {
        vm.assume(who != address(0));
        vm.deal(who, amount);
        vm.prank(who);
        jar.deposit{value: amount}();
        assertEq(address(jar).balance, jar.total());
    }
}

The test imports TipJarDeployer, which Tama will generate in step 6. The deployer embeds the exact bytecode the Verity compiler produced for your contract — the same bytes you’d put on-chain. The fuzz test and the invariant check are the executable shadow of the proof you just wrote.

Each // tama: mirrors=<spec> comment must sit directly above a testFuzz* or invariant_* function — putting a mirrors= tag on a plain test_* function is a build error. Tests without a mirrors= tag are ordinary Foundry tests and not tracked. The model is symmetric with the proof side: a spec is “covered” when at least one proof theorem discharges it and at least one Foundry test mirrors it.

Step 6 — Build everything

tama build

You’ll see something like:

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        2 manifests: ERC20Lite, TipJar
  run  trust-probe     Lean records proof dependencies for audit
  ok   trust-probe     trust-boundary inputs written
  run  solc            TipJar Yul through solc 0.8.33 standard JSON
  ok   solc            TipJar bytecode and hash written
  run  bridge          TipJar Solidity interface and deployer
  ok   bridge          TipJar bridge files generated
  run  forge           Foundry compiles generated bridges and tests
  ok   forge           forge build completed
Build completed: 2 manifests

If proof-check fails with unsolved goals, your proof script needs more help — Lean is telling you exactly where. Almost always the fix is to add a lemma name to the simp [...] list, or omega for arithmetic, or to do a case split on a hypothesis.

Step 7 — Run the audit

tama audit

You should see the five checks pass:

audit:
  ✓ structure       all files present, bytecode hashes match
  ✓ selectors       8 functions agree across Verity / manifest / Yul / Solidity
  ✓ storage-layout  no overlap, all encodings recognized
  ✓ coverage        every spec has a discharger and a mirror
  ✓ trust-boundary  no sorry, axioms allowlisted

The line that matters most is the last one. trust-boundary walks the Lean dependency graph of every theorem that discharges a spec and refuses any reliance on sorry or unallowlisted axioms. That’s the seal: the proofs are real, and they rest on a small set of named assumptions written down in tama.toml.

Step 8 — Watch the audit catch a bug

Let’s break the contract on purpose. Open verity/src/TipjarProtocol/TipJar.lean and introduce a leak in withdraw:

function withdraw(amount : uint256) external do
  let me := msg.sender
  require balances[me] >= amount
  balances[me] := balances[me] - amount
  -- forgot to subtract from total!
  transfer me amount

Now run:

tama build

You’ll see:

proof-check failed:
  TipJarProof.withdraw_preserves_invariant: unsolved goals

  pre.total - amount = (pre.total - amount).succ

Lean caught the inconsistency before any bytecode came out. The proof that the invariant survived withdraw is no longer true, because the implementation no longer matches the spec. Put the total := total - amount line back, rerun, and watch the build go green again.

This is the loop. Implementation and spec are kept honest by the proof. The proof is kept honest by Lean. The bytecode is kept honest by the manifest hash. The audit ties all three to a Foundry test you can run with one keystroke.

Where to go next

• Starter project walkthrough - walkthrough of a more advanced project ERC20Lite that implements & proves a subset of a ERC20 token.
• Concepts — every term used above (obligation, mirror, manifest, trust boundary), defined plainly with examples.
• Reading audit output — what each check actually inspects, what its failures look like, and how to fix them.
• Writing proof obligations — patterns for spec decomposition, frame conditions, and helper lemmas.
• CLI reference — every flag for every command.
• Verity EDSL reference — the language we wrote the contract in, in detail.
• Verity examples — the upstream contracts, each one introducing a new pattern.