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.

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.
  • Automatic support for nested mappings unless the pinned Verity compiler and Tama manifest adapter expose the required metadata.
  • 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 theorem that discharges a spec.
  • 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 and not listed in [trust.allow_surfaces].