Tama

What v0.1 doesn't do

Limitations

Tama v0.1 is intentionally narrow. Unsupported features must fail with a clear diagnostic before Tama emits bytecode, bridge files, or audit reports that imply stronger guarantees than the toolchain can provide.

Supported platforms

  • Linux x86_64
  • Linux aarch64
  • macOS x86_64
  • macOS aarch64

Native Windows is not supported in v0.1. Use WSL2 with the Linux x86_64 installer.

Supported project shape

Tama supports a flat Verity project layout:

verity/src/Foo.lean
verity/spec/FooSpec.lean
verity/proof/FooProof.lean
test/verity/Foo.t.sol

lakefile.toml is generated by tama init and user-owned after that. Tama edits it only on explicit dependency commands (install, remove, update, doctor --fix), and uses formatting-preserving edits.

Supported starter

The default starter is ERC20Lite. It exercises mappings, an ERC20-like transfer path, proof obligations, bridge generation, Foundry mirror tests, and audit.

The pinned Verity macro syntax used by the starter does not currently expose event declarations for verity_contract, so the generated ERC20Lite starter does not emit ERC20 Transfer events in v0.1. Event ABI parsing and manifest validation are supported for compiler outputs that do include event metadata. The Verity EDSL reference tracks what the language exposes as the framework moves forward.

Counter is a compatibility fixture, not the starter template.

Unsupported in v0.1

  • Windows artifacts and installer behavior.
  • Full Solidity feature parity.
  • ABI types outside the v0.1 supported subset: uint256, address, and bool.
  • Direct execution of arbitrary Verity monorepo Python scripts on Tama projects.
  • Automatic support for nested mappings unless the pinned Verity compiler and Tama manifest adapter expose the required metadata.
  • Arbitrary Yul semantic storage proofs.
  • User-edited generated files without the exact generated-file header.
  • Direct reliance on Foundry compiler settings for Verity Yul. Tama uses [yul] in tama.toml.
  • Hidden Foundry test filters. tama test is a passthrough to forge test.

Fail-closed by audit

These are accepted at build time but rejected by tama audit so they can’t reach a release:

  • sorry in any @[tama.obligation] theorem.
  • Axioms not listed in [trust.allow_axioms].
  • Raw event emission gaps where the manifest expects events.
  • Low-level call / delegatecall / proxy mechanics.
  • Runtime introspection.
  • Partially modeled linear-memory mechanics flagged by the compiler’s trust-surface report.