Tama

玉 Verity developer toolchain

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 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 the same audited bytecode you ship on-chain.

Write your first contract What is Verity?
curl -L https://tama.tools/install.sh | sh Install →
$ 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
scaffold a projectverify and compileaudit before release

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.

Implementation

The Lean EDSL describing what the contract does. Familiar shape: storage, functions, requires, returns. Compiles to Yul, then to EVM bytecode.

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.

Tama coordinates Lean, the Verity compiler, solc, and Foundry, and threads the manifest — a single JSON record per contract — through every stage. Audits read the same manifest, so the bytecode you ship and the properties you proved about it cannot drift apart.

Tama pipeline Verity source flows through Lean proof, Verity codegen to Yul, solc to bytecode, generated Solidity bridge files, and Foundry build. Audit checks branch off the manifest, bridge, and trust probe. Verity .lean Proof Lean elaborates Yul codegen Bytecode solc Bridge .sol Foundry forge build manifest — single source of truth trust-boundary selectors storage-layout structure coverage source artifact

Why bother

Tests find the bugs you thought of. Proofs cover the ones you didn't.

一

The bytecode you proved is the bytecode you ship.

Tama compiles Verity to Yul, then to bytecode, and records a SHA-256 of the result in the manifest. The deployer that goes on-chain embeds those exact bytes — not a Solidity reimplementation.

二

Foundry stays. Forge tests, fuzzers, scripts, RPCs — unchanged.

A Tama project is a Foundry project. Run forge test directly. Your invariant fuzz tests double as mirrors for the proven obligations, so the two views back each other up.

三

The trust boundary is small, named, and on the page.

tama audit trust-boundary walks the Lean proof and refuses any reliance on sorry or unallowlisted axioms. Every assumption has a name, a reason, and an entry in tama.toml.

入

Install in one command.

Detects your platform, fetches the signed release manifest, verifies the SHA-256, and drops tama + tamaup into ~/.tama/bin. No flags, no surprises.

curl -L https://tama.tools/install.sh | sh

Linux and macOS, x86_64 and aarch64. Read what it does first →

玉魂

Hard like jade. The soul of a system you can hold in your hand.

Begin →