Implementation
The Lean EDSL describing what the contract does. Familiar shape: storage, functions, requires, returns. Compiles to Yul, then to EVM bytecode.
玉 Secure by construction · Ethereum smart contracts
Tama
Tama means jade and soul. Hard, beautiful, and the inner truth of a thing.
Tama is the developer toolchain for Verity — a way of writing Ethereum smart contracts where you also write down, mathematically, what the contract must do, and a machine checks the proof. One CLI takes you from source, through proof and codegen, to deployable EVM bytecode — and the bytes you ship are the bytes the proof is about.
$ tama init my-protocol
✓ scaffolded ERC20Lite
✓ wrote tama.toml, lakefile.toml
✓ pinned verity 0.5.0
$ tama build
→ proof Lean elaborates
✓ proof modules accepted
→ codegen Yul + manifest
✓ solc bytecode written
✓ forge Foundry built
$ tama audit
✓ structure artifacts present
✓ selectors functions agree
✓ storage-layout no overlap
✓ coverage every obligation mirrored
✓ trust-boundary axioms allowlisted
Three layers, one truth.
A Verity contract is written three times — as code, as a specification, and as a proof that the two agree. Tama keeps all three in one project, in one build, in one verifiable artifact.
Specification
What the contract must do. Invariants, postconditions, frame conditions — the rules a correct implementation has to satisfy.
Proof
A machine-checked argument that the implementation satisfies the specification. No hand-waving, no "trust the developer." Lean checks every step.
The pipeline
From a Lean theorem to a hex string you can deploy.
Lean checks the proof. The compiler emits EVM bytecode. The manifest records the hash of both — so the bytes you deploy are, by construction, the bytes the proof is about.
Why bother
Tests find the bugs you thought of. Proofs cover the ones you didn't.
一
Every input. Every path. Every time.
A test checks the cases you wrote down. A Verity proof is a statement about every reachable state — every caller, every input, every interleaving. If the proof checks, no example can break it, because the proof is the universal example.
二
The spec is on the page, not in your head.
Writing the property down forces you to commit to what correct means. Reviewers and auditors read the same statement Lean does. When the spec is wrong, you can see it; when the implementation drifts, the proof breaks.
三
Whole bug classes become impossible.
Once an invariant is proven — balances sum to total supply, no path re-enters before settlement, no overflow on a critical sum — no future edit can quietly violate it. Tama re-checks the proof on every build.
入
Install in one command.
Linux and macOS, x86_64 and aarch64. Read what it does first →
curl -L https://tama.tools/install.sh | sh玉/魂
Hard like jade. True as soul.