Foundry interop

A Tama project is a Foundry project

tama init produces a directory that Foundry recognizes:

my-protocol/
├── foundry.toml         # standard Foundry config
├── lib/                 # Foundry deps (forge-std as a git submodule)
├── src/                 # Solidity sources (incl. src/generated/verity/)
├── script/              # Foundry deployment scripts
├── test/                # Foundry tests, incl. test/verity/ mirrors
├── out/                 # Foundry build output
└── cache/               # Foundry cache

…plus the Verity layers (verity/src, verity/spec, verity/proof) and the Tama-owned bits (tama.toml, tama.lock, lakefile.toml, artifacts/).

You can cd into the project and run any forge command. Tama does not wrap or reinterpret Foundry; the tama test command is exactly forge test [args] with no injected filters.

Who owns which file

File	Owned by	Edited by
foundry.toml	You	You
tama.toml	You	You
tama.lock	Tama	tama init, build, update
lakefile.toml	You (after init)	You; tama install/remove/update/doctor --fix
lake-manifest.json	Lake	lake update (via Tama)
lean-toolchain	You	You
src/generated/verity/*	Tama	tama build
artifacts/**	Tama	tama build, tama audit
test/verity/*	You	You
lib/**	Foundry	forge install, forge update

The two configs are intentionally non-overlapping:

• Solidity compilation, fuzzing, RPC endpoints, profiles, remappings → foundry.toml.
• Verity paths, generated bridge paths, Yul solc settings, trust-boundary policy → tama.toml.

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

When to use forge directly

Task	Command
Run all tests	tama test (or forge test)
Run a specific test	tama test --match-contract FooTest
Run with verbosity	tama test -vvv
Install a Solidity dep	forge install owner/repo
Remove a Solidity dep	forge remove owner/repo
Update Solidity deps	forge update
Inspect a non-Verity contract	forge inspect Foo abi
Run a script	forge script ...
Test gas snapshots	forge snapshot

Use tama test whenever you would have used forge test — it preserves all arguments, exit codes, and output. Tama’s --offline flag is the one thing translated to forge’s --offline.

For inspecting Verity-generated contracts, use tama inspect, which reads the manifest. For inspecting plain Solidity contracts, use forge inspect.

Mirror tests run in plain Foundry

A mirror test is just a Foundry test under test/verity/. It imports the generated Iface and Deployer and exercises the real Verity bytecode. The link to a spec is a // tama: mirrors=<spec> comment directly above the test function — forge test does not need to know about it.

import {TipJarIface} from "src/generated/verity/TipJarIface.sol";
import {TipJarDeployer} from "src/generated/verity/TipJarDeployer.sol";

contract TipJarTest is Test {
    TipJarIface jar;

    function setUp() public { jar = TipJarDeployer.deploy(); }

    // tama: mirrors=total_tracks_balances
    function invariant_totalTracksBalances() public view {
        assertEq(address(jar).balance, jar.total());
    }

    // tama: mirrors=total_tracks_balances
    function testFuzz_deposit(address who, uint96 amount) public {
        vm.assume(who != address(0));
        vm.deal(who, amount);
        vm.prank(who);
        jar.deposit{value: amount}();
        assertEq(address(jar).balance, jar.total());
    }
}

The function above each mirrors= tag must be named testFuzz* or invariant_*; putting the tag on a plain test_* function is a build error. Multiple comma-separated spec names are allowed (mirrors=foo,bar, no whitespace after commas), and any number of tests can mirror the same spec.

tama audit coverage is what closes the loop: it reads each mirrors= tag, checks that the named spec exists, and ensures every spec ends up with at least one mirror (or a [coverage.proof_only] entry).

Generated files are off-limits

Files under src/generated/verity/ start with:

// GENERATED by tama; do not edit.

Tama refuses to overwrite a generated file whose first line has been altered — this is a safety net so a hand edit isn’t silently lost. But a clean regeneration during the next tama build will overwrite it. Don’t put logic in generated files. Move it into verity/src/Foo.lean (if it’s contract logic) or into a user-owned Solidity file (if it’s adapter glue).

A simple mental model

Tama owns Verity. Foundry owns Solidity. The two meet at the manifest and the generated bridge files. Everything else is one or the other.