What tama audit is for

tama audit is a release-time gate that runs after a successful tama build. Each check inspects the build artifacts (manifests, generated bridges, bytecode files, trust probes) and asks one focused question. The full suite is:

structure        Required files and bytecode hashes
selectors        Function/event/error selectors agree everywhere
storage-layout   Slot allocation is sane and consistent
coverage         Every spec has a discharger and either a mirror or a proof-only reason
trust-boundary   Lean axioms, sorry, unresolved declarations

Run them all with tama audit. Run one with tama audit <check>. Pass --deny-warnings in CI to fail on warning-severity findings.

structure

What it inspects:

  • Every contract has the expected verity/src/, verity/spec/, verity/proof/, test/verity/ files.
  • Every manifest’s referenced artifacts (Yul, solc JSON, bytecode, generated interface, generated deployer) exist on disk.
  • The bytecode_hash recorded in each manifest matches the SHA-256 of the actual creation bytecode file.
  • The bytecode embedded in each generated Deployer.sol matches the bytecode the manifest points to.

A real failure:

structure: error
  ERC20Lite: deployer bytecode does not match manifest

    expected (manifest.bytecode_hash):
      9c…3e
    actual (src/generated/verity/ERC20LiteDeployer.sol embedded):
      a1…77

  This usually means the deployer was regenerated, then the bytecode
  was rebuilt without re-running bridge generation. Run `tama build`
  again.

The fix is almost always tama build. If that doesn’t clear it, you have a hand-edited generated file — see Generated artifacts.

selectors

What it inspects:

  • Function selectors derived from Verity declarations.
  • Function selectors recorded in the manifest ABI.
  • Function selectors declared by the generated Solidity interface.
  • Function selectors used in the generated Yul dispatcher.
  • The keccak-derived expected selector from the canonical signature.

All five must agree. Custom error selectors and event topic0 values go through the same check.

A real failure:

selectors: error
  TipJar.deposit: selector mismatch

    Verity declaration: 0xd0e30db0   deposit()
    Manifest entry:     0xd0e30db0
    Solidity iface:     0xd0e30db1   ← mismatch
    Yul dispatcher:     0xd0e30db0

This is almost always evidence that a generated file was hand-edited. Restore the file and run tama build.

storage-layout

What it inspects:

  • Each storage variable’s declared slot is a valid uint256.
  • No two variables share a slot (unless the offsets and widths permit it).
  • Mapping/array encoding tags are recognized by Tama.
  • The compiler’s reported layout matches the manifest layout.

A real failure:

storage-layout: error
  TipJar: slot 0x01 used by both `balances` and `total`

  balances : mapping(address, uint256)  slot 0x01 offset 0  width 32
  total    : uint256                    slot 0x01 offset 0  width 32

  Edit the source so each variable has a distinct base slot, or use
  Verity's storage layout helpers to pack them explicitly.

coverage

What it inspects:

  • Every spec has at least one discharger AND either at least one Foundry mirror or a [coverage.proof_only] entry in tama.toml.
  • Every spec has at least one discharger that tama build discovered in the proof namespace — a theorem whose conclusion (after stripping non-Prop binders) is the spec application or a positive conjunction containing it.
  • Every // tama: mirrors=<spec> tag sits directly above a function named testFuzz* or invariant_*, and names a real spec in some contract.
  • Every [coverage.proof_only] key matches a real obligation id (<Contract>.<spec_name>).

A real failure:

coverage: error
  TipJar.total_tracks_balances: no mirror and no [coverage.proof_only] entry

    spec:        verity/spec/TipjarProtocol/Spec/TipJarSpec.lean:total_tracks_balances
    dischargers: TipJarProof.deposit_preserves_invariant
                 TipJarProof.withdraw_preserves_invariant

    Add a `// tama: mirrors=total_tracks_balances` comment above a
    `testFuzz_*` or `invariant_*` function in test/verity/TipJar.t.sol,
    or list it under [coverage.proof_only] in tama.toml with a reason.

trust-boundary

What it inspects:

  • For every spec, the closure of axioms, unsafe declarations, and unresolved names reachable from each of its dischargers (via Lean’s collectAxioms). Every spec’s dischargers must walk to allowlisted axioms only.
  • Compiler trust-surface artifacts (artifacts/trust-report.json, artifacts/assumption-report.json).

The compiler artifacts come straight from the Verity framework; see Verity’s TRUST_ASSUMPTIONS.md for what the framework itself takes on trust before any project-level allowlist enters the picture.

A real failure:

trust-boundary: error
  TipJarProof.withdraw_preserves_invariant
    depends on: sorryAx

  `sorry` is denied for any theorem that discharges a spec. Replace the
  sorry with a real proof, or change the theorem so its conclusion no
  longer matches the spec.

trust-boundary: warning
  TipJarProof.deposit_preserves_invariant
    depends on: Classical.choice (not in [trust.allow_axioms])

  Add to tama.toml:

    [trust.allow_axioms]
    "Classical.choice" = "accepted Lean classical reasoning"

trust-boundary: error
  TipJar [function:withdraw]
    uses: contractAddress (not in [trust.allow_surfaces])

  Add to tama.toml only after reviewing the generated trust report:

    [trust.allow_surfaces]
    "contractAddress" = "address introspection is reviewed and intentional"

CI patterns

Standard CI:

- run: tama build --locked
- run: tama test
- run: tama audit

Stricter release CI:

- run: tama doctor
- run: tama build --locked
- run: tama test
- run: tama audit --deny-warnings
- run: tama audit trust-boundary
- run: tama audit coverage

The two extra individual tama audit <check> calls produce focused output and exit codes when the suite is being driven by a release pipeline that wants to record per-check results separately.