tama.toml & tama.lock

`tama.toml`

tama.toml has four roles:

mark the project as a Tama project;
pin the intended Verity framework version;
define Verity/Tama-side paths;
define Yul compilation and audit policy.

Full example:

[project]
name = "my_protocol"
verity = "0.5.0"

[paths]
src = "verity/src"
spec = "verity/spec"
proof = "verity/proof"
mirror_test = "test/verity"
generated_solidity = "src/generated/verity"
out = "artifacts"

[modules]
src = "MyProtocol"
spec = "MyProtocol.Spec"
proof = "MyProtocol.Proof"

[yul]
solc = "0.8.33"
evm_version = "cancun"
optimizer = true
optimizer_runs = 200
yul_optimizer = true
metadata_bytecode_hash = "none"

[trust.allow_axioms]
"Classical.choice" = "accepted Lean classical reasoning"
"Quot.sound"       = "accepted Lean quotient axiom"

[trust.allow_surfaces]
"contractAddress" = "address introspection is reviewed and intentional"
"tload/tstore"    = "transient storage is reviewed and intentional"

[coverage.proof_only]
"Foo.mapping_collision_free" = "quantifies over all key pairs; no concrete fuzz schedule covers it"

`[project]`

Key	Required	Description
`name`	yes	Project name (matches `lakefile.toml`).
`verity`	yes	Verity framework tag or commit. Pinned in lock.

`[paths]`

Optional. Omitted fields fall back to the defaults shown above.

Every path must be a non-empty relative path inside the project. Absolute paths, .. components, and root-collapsing values like . are rejected before Tama writes or removes anything.

When Tama also consumes Foundry paths (src, test, out, cache_path in foundry.toml) for audit and clean behavior, the same project-relative rule applies.

`[modules]`

Optional for existing projects. New projects created by tama init include this table so Lean modules live under the package root instead of the legacy TamaSrc/TamaSpec/TamaProof aggregate modules.

Key	Description
`src`	Lean module root for files under `[paths].src`.
`spec`	Lean module root for files under `[paths].spec`.
`proof`	Lean module root for files under `[paths].proof`.

For the example above, an implementation file at verity/src/MyProtocol/ERC20Lite.lean is module MyProtocol.ERC20Lite, and the aggregate source module is verity/src/MyProtocol.lean. tama init my-protocol derives these roots from the package name: MyProtocol, MyProtocol.Spec, and MyProtocol.Proof.

`[yul]`

Key	Default	Description
`solc`	required	`solc` version Tama uses for generated Yul.
`evm_version`	`cancun`	EVM target.
`optimizer`	`true`	Enable the Yul optimizer.
`optimizer_runs`	`200`	Optimizer run count.
`yul_optimizer`	`true`	Enable the standalone Yul optimizer step.
`metadata_bytecode_hash`	`"none"`	Reproducible bytecode by default.

metadata_bytecode_hash = "none" is intentional: it removes the non-deterministic Solidity metadata trailer from the generated bytecode, so the manifest’s recorded hash is reproducible across machines.

`[trust.allow_axioms]`

A map of axiom-name -> reason. Each reason must be a non-empty string.

sorryAx cannot be allowlisted. tama audit trust-boundary denies it unconditionally.

`[trust.allow_surfaces]`

A map of Verity compiler-reported trust surface identifier to reason. Each reason must be a non-empty string.

Use the exact identifier reported by artifacts/trust-report.json, for example contractAddress, tload, tstore, or tload/tstore. These entries acknowledge compiler-modeled or partially modeled EVM features; they do not allow Lean axioms or sorryAx.

`[coverage.proof_only]`

A map of fully qualified obligation id ("<Contract>.<spec_name>") to a non-empty reason string. Use this to mark specs that have no useful executable shadow — typically those that quantify over symbolic state in a way no fuzz schedule could cover.

[coverage.proof_only]
"Foo.mapping_collision_free" = "quantifies over all key pairs; no concrete fuzz schedule covers it"

Validation:

The key must match a real obligation id (i.e. a top-level def in some verity/spec/<Contract>Spec.lean file). An unknown key is a build error.
The value must be a non-empty trimmed string. An empty or whitespace-only reason is a config-load error.

tama audit coverage accepts a spec with a [coverage.proof_only] entry as covered without requiring a Foundry mirror; the reason is audit-visible. Specs not listed here must be mirrored by at least one testFuzz*/invariant_* function tagged // tama: mirrors=<spec>.

Strict parsing

tama.toml is strict: unknown Tama-owned table names or keys are errors, not warnings. This prevents misspelled compiler or path settings from silently changing build behavior. Foundry-specific settings remain in foundry.toml and are parsed by Foundry.

`tama.lock`

Resolved state for reproducible builds. Tama writes it on init, refreshes it after a successful build, validates it under --locked, and reports drift via doctor.

version = 1

[resolved]
verity_version = "0.5.0"
verity_git     = "https://github.com/lfglabs-dev/verity"
verity_rev     = "3a6f..."
lean_toolchain = "leanprover/lean4:v4.22.0"
solc           = "0.8.33"
solc_sha256    = "..."

[inputs]
tama_toml_sha256      = "..."
lakefile_toml_sha256  = "..."
lake_manifest_sha256  = "..."
foundry_toml_sha256   = "..."

[yul]
evm_version            = "cancun"
optimizer              = true
optimizer_runs         = 200
yul_optimizer          = true
metadata_bytecode_hash = "none"

[resolved.lake]
"verity"        = { rev = "3a6f...", url = "https://github.com/lfglabs-dev/verity" }
"verity-erc20"  = { rev = "1c2d...", url = "https://github.com/lfglabs-dev/verity-erc20" }

Rules

tama init writes the initial lockfile.
tama build refreshes the lockfile after a successful build.
tama build --locked (and CI) fails if the lockfile or any tracked input is stale.
tama update recomputes the lockfile after refreshing dependencies.
tama doctor reports drift; tama doctor --fix may apply narrow, formatting-preserving repairs.

`[resolved.lake]`

Direct git packages from lake-manifest.json are recorded here so the lock captures Lake’s actual resolved commit, not just the requested branch or tag in lakefile.toml.

Relationship to other configs

File	Owned by	Purpose
`tama.toml`	You	Verity pin, paths, Yul, audit policy
`tama.lock`	Tama	Resolved versions and input hashes
`foundry.toml`	You	Solidity compiler, fuzz, profiles, RPC, etc.
`lakefile.toml`	You (after `tama init`)	Lake build targets and Lean dependencies
`lake-manifest.json`	Lake	Resolved Lake dependency graph
`lean-toolchain`	You	Pinned Lean toolchain

Tama does not read foundry.toml to configure Yul. Foundry does not read tama.toml. The two share the project on disk, not in memory.