What counts as an obligation

An obligation is any top-level definition in the spec file verity/spec/<Contract>Spec.lean. The spec file is pure Lean: every top-level def and every #gen_spec invocation is automatically an obligation tracked in the manifest. There are no -- tama: comments in the spec file.

The build rejects a spec file that contains anything other than import, namespace, open, def, #gen_spec, and end. In particular, lemmas and auxiliary defs used only as helpers must live outside the spec file — typically in a sibling Lean module that the spec or proof imports.

import Foo

namespace FooSpec

def total_in_range (s : Foo.State) : Prop :=
  s.total ≤ s.cap

def mint_increases_total
    (pre post : Foo.State) (call : Foo.Call) : Prop :=
  post.total = pre.total + call.amount

end FooSpec

tama audit coverage requires every spec to have at least one discharger AND either at least one Foundry mirror test or a [coverage.proof_only] entry in tama.toml.

Discharging via proof

In the proof file verity/proof/<Contract>Proof.lean, write the theorems that discharge your obligations with no Tama annotations — dischargers are auto-discovered by type:

namespace FooProof

theorem mint_preserves_total_in_range
    (pre : Foo.State) (call : Foo.Call) :
    FooSpec.total_in_range_after_mint pre call := by
  unfold FooSpec.total_in_range_after_mint
  intro h k
  simp [Foo.mint, h, k]
  omega

end FooProof

During tama build, Tama enumerates the theorems in the proof namespace from the elaborated Lean environment. For each one it strips the leading non-Prop binders (the data inputs) and inspects the conclusion. A theorem discharges a spec when that conclusion is the spec application directly, or a positive conjunction containing it — so a single theorem that proves a conjunction discharges every spec named in the conjunction:

theorem mint_combined
    (pre : Foo.State) (call : Foo.Call) :
    FooSpec.total_in_range pre call ∧ FooSpec.mint_increases_total pre call := by ...

Discovery is file-layout independent: the proof may be split across imported submodules, since all of them share the proof namespace. Tama finds the theorems wherever they live.

The discharge criterion is exactly the elaborated conclusion. A theorem discharges a spec only if, after stripping non-Prop binders, its conclusion is the spec application or a positive conjunction containing it. True, unrelated specs, P -> spec ..., disjunctions, existentials, and helper-position mentions do not discharge the spec. Put preconditions inside the spec definition, then unfold the spec in the proof and introduce those assumptions there.

Theorems whose conclusion is anything else are treated as helpers — they never appear in the manifest. There is nothing to tag: write the obligation-closing theorems in the spec-application shape and leave the scaffolding alone.

Discharging via mirror

In a Foundry test file (typically test/verity/<Contract>.t.sol), each fuzz/invariant test that mirrors a spec carries a // tama: mirrors=<spec_name> Solidity comment directly above the function declaration:

// tama: mirrors=mint_increases_total
function testFuzz_mintIncreasesTotal(uint96 amount) public {
    uint256 before = foo.total();
    vm.assume(before + amount <= foo.cap());
    foo.mint(amount);
    assertEq(foo.total(), before + amount);
}

The same comma-separated rule applies (mirrors=foo,bar, no whitespace after commas), and multiple tests may mirror the same spec.

The function name must start with testFuzz or invariant_. Putting a mirrors= tag on a plain test_* function is a build error — the point is that mirrors are property-shaped: they exercise the same universal statement the spec made, on real bytecode, under random inputs. A name on the right of mirrors= that isn’t a known spec (any contract) is also a build error.

Tests without a mirrors= tag are ordinary Foundry tests and never appear in the manifest.

Proof-only obligations

Some properties are intrinsically about symbolic state and have no useful executable shadow — for instance, “the storage encoding is collision-free for any pair of distinct mapping keys.” List these in tama.toml under [coverage.proof_only], keyed by the fully qualified obligation id (<Contract>.<spec_name>):

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

The reason is required and audit-visible. An empty or whitespace-only reason is a config-load error. A key that doesn’t match any real obligation id is a build error.

sorry is fine — until release

Lean lets you write sorry in the middle of a proof to come back to it later. tama check and tama build accept sorry. tama audit trust-boundary denies it, every time, no allowlist.

The intent: keep working contracts in a half-proven state during development; gate releases on a real proof.

theorem withdraw_drops_total : ... := by
  sorry  -- ok locally, will fail audit

Allowlisted axioms

Lean’s standard library uses a few classical axioms that are universally accepted in mathematics but not part of bare type theory. To allow them explicitly:

# tama.toml
[trust.allow_axioms]
"Classical.choice" = "accepted Lean classical reasoning"
"Quot.sound"       = "accepted Lean quotient axiom"
"propext"          = "function extensionality on propositions"

The string is the audit-visible reason. Don’t allowlist anything you can’t defend in two sentences. Verity itself ships with zero documented axioms; anything you allowlist is a project-level choice, not a framework one.

Where to look when a proof won’t close

  • tama check runs spec elaboration without proofs. If your spec file has a type error, tama check finds it in seconds.
  • tama build with --verbose shows the Lake invocation and full Lean output, including the goals at the failure site.
  • Inside Lean, simp? and exact? will often suggest the lemma name you’re missing; omega closes nearly all linear arithmetic goals; decide closes small decidable propositions.
  • Verity’s debugging-proofs guide catalogues the common error messages and tactic patterns from the Verity side — start here before reaching for sorry.
  • Read the audit guide — many “proof failures” are actually structural mistakes (e.g. a spec with no theorem whose conclusion is its application, or a theorem target that does not actually contain the spec application) that the build reports before audit inputs are written.