tama玉 / 魂
Install
玉の如く堅く、魂の如く真。

Provably secure Ethereum smart contracts.

Tama is the toolchain for Verity. You write the contract, you write down what correct behavior looks like, and Lean checks that one matches the other. A single CLI takes you from source to proof to deployable EVM bytecode.

$curl -L https://tama.tools/install.sh | sh
Linux and macOS, x86_64 and aarch64. See what the script does before you run it.
CA0x34329388c693e830b6dd2cb5268d98fcf242345e
Start a project How it works
verity/src/ERC20Lite.lean
Try breaking it, then build again
Press tama build to check the proof and compile the contract.

ERC20Lite proved

obligations11 / 11
mirror tests10 bound
sorryAxnone
bytecode0x7c1e…a94f

Three steps to a contract you can prove.

Every contract in a Tama project lives in three files. Lean reads all three, and the build only passes when the third one holds.

1Code

Write the contract itself in Verity, a Lean EDSL that reads like Solidity. It compiles to Yul, then to EVM bytecode with a pinned solc.

verity/src/Token.lean 

      

      

        
2Spec

        
Define what correct behavior looks like: invariants, postconditions, and what a call must leave untouched. Each top-level definition becomes an obligation Tama tracks.

        verity/spec/TokenSpec.lean
        

      

      

        
3Prove

        
Prove the code matches the spec. Lean accepts the proof or rejects it, and there is no middle ground. Tama links each theorem to the obligation it discharges.

        verity/proof/TokenProof.lean
        

      

    

  










  

    

      
A fuzzer tries inputs. A proof covers all of them.

      
Tests check the cases someone thought to write, and fuzzers sample more. A proof is a statement about every reachable state, so the bug in the corner nobody sampled has nowhere to hide.

    

    

      

        
Fuzzing0 runs

        
        
sampled statenever visited

      

      

        
Proof0%

        
        
covered by the theoremcounterexample, build fails

      

    

    

      
Every reachable state
A theorem quantifies over all inputs and all storage, not just the inputs a test author or a fuzzer happened to pick.

      
The spec is written down
Reviewers and auditors read the same statement Lean checks. What the contract promises stops living only in someone's head.

      
Re-checked on every build
Once an invariant is proven, Tama checks it again on each build, so a later edit can't quietly break it.

    

  










  

    

      
The proof and the bytecode share one hash.

      
Verity source is checked as a Lean proof and compiled to EVM bytecode in the same build. The manifest records the same hash for both, so the bytes you deploy are the bytes the proof is about.

    

    

      

        
          
            
          
          
            
            
            
            
            
          
          
            
            
            
            
          
          
            
            Verity source
            src + spec + proof

            
            Lean proof
            kernel checked

            
            Yul
            Verity codegen

            
            bytecode
            pinned solc

            
            manifest
            hash 0x7c1e…a94f
          
        
        
provedVerity semantics and the compiler layers down to Yul.
pinnedsolc turns Yul into bytecode, recorded in tama.lock.
linkedOne manifest per contract ties the proof to the deployed bytes.

      

      

        
artifacts/manifest/ERC20Lite.jsontama.contract-manifest.v1

        

      

    


    

      

        
Proofs on the model, tests on the real bytes.

        
Every obligation needs a Lean theorem that discharges it, and a Foundry fuzz test or invariant that mirrors it on the emitted bytecode. One comment links the two. If a spec is proof-only, you say so in tama.toml and give a reason.

        
    
          
  • FooIface.sol the ABI interface, regenerated each build
    • 
          
  • FooDeployer.sol deploys the exact bytecode the proof covers
    • 
          
  • tama.lock pins the Verity revision, Lean toolchain and solc
    • 
        

      

      

    

  










  

    

      
One CLI, from scaffold to audit.

      
Tama wraps Lean, Lake, Verity codegen, solc and Foundry behind a handful of commands, and pins all of them so CI builds what you built.

    

    

      

        

        

      

      

        
tama initScaffold a Foundry-shaped project with an ERC20Lite starter.

        
tama doctorCheck the CLI, Lean and Lake, Foundry, solc, Git and the lockfile.

        
tama checkBuild the code and spec quickly, skipping proofs, while you edit.

        
tama buildProofs, codegen, manifest, solc, Solidity bridge and forge build.

        
tama testRun the Foundry tests, including mirrors bound to specs.

        
tama auditArtifacts, selectors, storage layout, coverage and trust boundary.

        
tama inspectRead the manifest, ABI, storage layout, obligations or trust set.

      

    

  










  

    

      
Every assumption has a name.

      
A proof is only as good as what it rests on. The trust boundary is the set of axioms, unsafe declarations and compiler assumptions your proofs depend on. Tama doesn't pretend it's empty. It makes it visible and makes you sign off on it.

      
tama audit trust-boundary always rejects sorry, the marker Lean uses for an unfinished proof.

    

    

      
sorryAxAn incomplete proof. Never allowed into a release.
always denied

      
Classical.choiceStandard axiom of choice, usually allowlisted.
allowlisted

      
Quot.soundQuotient soundness, usually allowlisted.
allowlisted

      
your.custom.axiomAnything else stays out until you add it to the allowlist in tama.toml.
denied by default

      
solc: Yul to bytecodeThe final compile step runs on a pinned solc and is trusted, not proved.
trusted, pinned

    

  







  

    

      

        
Start from verified building blocks.

        
Tamago is a library of common contracts written in Verity and built with Tama, the way solmate and solady serve Solidity. Each one is proved in Lean and mirrored by Foundry tests.

      

      

        
OwnableSingle-owner access control with transfer and renounce.

        
ERC20Allowances, owner-controlled mint and burn, 18 decimals.

        
ERC721Approvals, operator approvals, minting and transfers.

        
WETHDeposits, withdrawals, approvals and transfers.

        
ERC4626Share and asset previews, deposit, mint, withdraw, redeem.

        
FixedPointMathLibUnsigned math helpers including roots, logs and clamping.

      

      
First formally verified EVM implementations ofsqrt()cbrt()log10()log256()ERC4626

      
$tama install Bacon-labs/tamago

    

  







  

    
    

      

        
Checked by Lean, the language mathematicians use to prove theorems.

        
Lean is a proof assistant and a programming language. Mathematicians, Terence Tao among them, use it to check real proofs line by line. Tama puts that same checker behind your contract, so "it's correct" becomes a statement a machine has verified.

      

      

        
玉
Jade. The code and its proof, hard enough that later edits can't chip them.

        
魂
Soul. The spec, the part that says what the contract is for.

      

    

  







  

    
Prove your first contract today.

    
Install Tama, run tama init, and you have a starter ERC20 with eleven obligations already proved.

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

    
Read the getting started guideView on GitHub

  









Copied