The deliverable is written, but I could not run forge on this machine. Every shell command, including a bare echo, fails before it starts with this sandbox error:

apply-seccomp: write /proc/self/setgroups (nested userns is capability-restricted; caller must provide CAP_SYS_ADMIN): Permission denied

The sandbox override is disabled in this session and reads outside the repository are blocked, so I could neither execute forge build, forge test and forge fmt --check nor clone forge-std. I wrote the whole project by hand and reviewed it against the 0.8.26 compiler rules, so the verifier's run is the first real build.

What was built

• src/MADToken.sol: a self-contained ERC-20 named Mutually Assured Destruction, symbol MAD, 18 decimals. The constructor mints 1,000,000,000 tokens once to msg.sender and takes no arguments. It has a holder-only burn, no owner, no mint path, no pause or block list, no external calls, and untaxed transfers so the launch flows move exactly what they say.
• test/MADToken.t.sol: 28 tests across metadata, the constructor mint and event, every transfer, approve and transferFrom success and failure path, burn, rejection of mint and admin selectors, ether rejection, and four fuzz tests for supply conservation and exact accounting. Every actor is a pranked constant address and no environment variables are read.
• lib/forge-std/: a minimal vendored subset of forge-std as plain files, with the Vm cheatcodes the tests use and a Test base whose assertions revert on failure.
• foundry.toml: pins solc = "0.8.26", sets bytecode_hash = "none", optimizer on, and the forge-std remapping. No ffi, no filesystem permissions.
• README.md: behaviour, assumptions, the launch's deployment parameters and supply flow, an After launch section stating there is nothing to configure, operational responsibilities, and a walk through the security checklist.

What is unverified

• Compilation, test results and formatting could not be checked here. The main risk is a compile error in the hand-written files, which the verifier will surface. Formatting is applied by the post-processing step, so forge fmt --check depends on that running.

Created launch.json matching MADToken, its argument-free constructor, exact supply, and required pool/economics settings.

Validation passed. forge build succeeded; all 29 tests passed with the supplied fuzz seed. Only launch.json is changed for submission.

The review is complete and .imd-findings.json holds one finding plus eight coverage rows.

Result: the token has no privileged surface at all, so the Access Control and Trust Gap guides find nothing to exploit. No owner, roles, modifiers, initializer, pause, blocklist, burnFrom, receive or fallback exist. The constructor takes no arguments and mints the whole supply to the factory. All four entry points are caller-bound and their balance and allowance guards hold for every non-zero amount. The sum-of-balances invariant holds through every writer.

One low finding, from the Asymmetry guide:

• transferFrom at src/MADToken.sol:89 accepts address(0) as the sender. transfer can never have a zero sender, and _transfer rejects a zero receiver, but nothing rejects a zero from. With amount zero both guards pass trivially, so any caller can emit Transfer(address(0), anyone, 0), which the contract's own NatSpec defines as a mint. No balance or supply changes, so the harm is limited to indexers and explorers that key on zero-address senders. The suggested fix is a zero-sender check mirroring the receiver check.
• The scratch test at test/scratch/ZeroSenderTransferFrom.t.sol fails on the current code, with the trace showing the spurious event. It is attached as the finding's proof.

Coverage: approve, burn and transfer hold. transferFrom carries the finding. Supply-only-shrinks, no-privileged-freeze, balance-conservation and deployment-role invariants hold. The aderyn large-literal lead is correct code and was not reported. Nothing in the tracked tree was modified.

The review is complete with no defects found in the assigned area. The findings file is valid JSON, the scratch directory is removed, and git status --porcelain shows a clean tree apart from the ignored .imd-findings.json.

Result: no findings. The token at src/MADToken.sol is a plain fixed-supply ERC-20 with a caller-only burn, no owner, no external calls and no constructor arguments. Checked against the Economic Security, Invariant and Flow Gap guides, every failure mode they list either has no surface here or was shown to hold.

What I verified, beyond reading:

• Conservation and monotonic supply. A scripted fuzz of random 12-step sequences across transfer, approve, transferFrom and burn, including the token contract itself as a receiver, kept the sum of balances equal to the supply, never let the supply grow, and never credited the zero address. It ran 3000 times without a counterexample.
• Launch flow exactness. The factory-to-distributor transfer, a distributor claim, a PoolManager-style sync/settle balance delta for the seed, a trader buy and sell, and a router transferFrom all moved exactly the amount asked.
• Sentinel and boundary cases. Zero receiver and zero spender revert. Transfers and burns of the max uint and of balance plus one revert rather than wrap. Self-transfer and self-transferFrom conserve the balance. A zero-amount transferFrom from the zero address is a no-op on state.
• Bytecode. The reachable-opcode scan found no DELEGATECALL, CALLCODE or SELFDESTRUCT, and the runtime is well under the EIP-170 limit. The compiled ABI exposes only the four listed state-changing functions.
• The existing test suite builds and passes with 29 tests.

Coverage record. All four entry points are marked holds, with four extra rows for the invariants above. One row is marked unreached: the deployment parameters in README.md, such as the FWA pair address and the economics split, could not be checked because no launch.json, network.json or job text is in the tree. Those values are documentation and do not feed the token's code.

Trust assumptions, not defects. The standard ERC-20 approve race is documented in both the source and the README. Tokens sent to the token contract itself are unrecoverable by design, and the README says so.

The review is complete and .imd-findings.json holds one finding plus a nine-row coverage record. No source files were changed; the scratch tests were removed.

What I reviewed. The token is a single 138-line contract, src/MADToken.sol, with no libraries, no external calls and no admin surface. I applied the Senior Auditor's Mindset and the three assigned guides: Execution Trace (parameter divergence, sentinel paths, unchecked arithmetic, partial updates, approval residuals), Periphery (the vendored forge-std subset, the only helper code in the tree) and First Principles (every implicit assumption behind the unchecked blocks and the launch flows). Build, the project's 29 tests and forge fmt --check all pass. I also scanned the compiled runtime for DELEGATECALL, CALLCODE, SELFDESTRUCT, CALL and CREATE, fuzzed 2000 random 24-step transfer/transferFrom/burn sequences against the sum-of-balances invariant, and traced the launch flow hop by hop. All held.

Finding (low). transferFrom(address(0), x, 0) is accepted. The receiver is validated at src/MADToken.sol:113 but the sender never is, so any caller can emit a zero-value Transfer from the zero address, which the contract's own NatSpec defines as a mint. OpenZeppelin v5 rejects this with ERC20InvalidSender. A non-zero amount reverts on allowance, so no balance or supply changes. Impact is confined to off-chain consumers that treat Transfer-from-zero as a mint. Minimal fix: add a from == address(0) revert at the top of _transfer.

Coverage. approve, burn and transfer hold. transferFrom carries the finding above. Extra rows cover the supply invariant, the absence of any mint or privileged path, the opcode scan, the constructor mint and the vendored test base. Nothing was left unreached.

Leads not reported. Aderyn's large-numeric-literal line is style only. The approve overwrite race is standard ERC-20 and documented. The launch-level parameters in the README (paired currency, fee, tick spacing, remainder address) are not code in this repository and belong to the manifest step.

I added two test files beside the existing test/MADToken.t.sol, and I found no defects in src/MADToken.sol. With the verifier's fuzz seed, forge build and forge test pass: 59 tests (29 existing, 29 new edge-case tests, and one invariant suite of 7 invariants). Nothing outside test/ was changed.

test/MADToken.invariant.t.sol: random call sequences

• A handler contract deploys the token, passes the supply to the first of five actors, and then makes random calls with bounded amounts.
• It calls the normal operations (transfer, approve including unlimited, transferFrom, burn) and five failure paths: sending more than the balance, sending to the zero address, spending more than the allowance, burning more than the balance, and approving the zero address. Each failure must revert with exactly the expected error and change nothing.
• It runs 256 runs × 64 calls, set in the test file because foundry.toml is off-limits. It is set to fail if any call reverts unexpectedly, and every operation was called and none reverted.
• The 7 invariants are:
  • the supply always equals the original mint minus everything burned;
  • the supply never goes up;
  • all balances add up to the supply, and nothing sits with the deployer, the token contract or the zero address;
  • each balance matches the handler's own running record (ghost value);
  • each allowance matches its ghost value;
  • every failure path behaved as expected;
  • name, symbol, decimals and the initial supply never change.
• Checked that it can fail: I temporarily broke burn so it reduced the supply by only half the amount. Two invariants failed (supply = minted − burned, and balances add up to the supply). I then restored src/ from git.

test/MADToken.edge.t.sol: edge cases and launch flow

• Launch flow: a factory-style contract deploys the token with CREATE2 and receives the whole supply. In one call it pays out 10% / 82% / 8% to the distributor, pool and requester, and each share arrives exactly. A distributor claim also arrives in full. Two different salts give two independent tokens; reusing a salt reverts.
• Zero amounts: burning 0 is allowed and still emits an event; transferFrom of 0 needs no allowance; sending 0 to the zero address still reverts; approving 0 clears an allowance.
• Allowance limits:
  • only exactly the maximum value counts as unlimited (max − 1 goes down when spent);
  • an unlimited allowance still can't move more than the balance;
  • spending your own tokens through transferFrom still needs an allowance;
  • an allowance from one owner gives nothing over another owner's tokens.
• Failure order: the allowance is checked before the balance, and a failed transferFrom leaves the allowance unchanged. Transfers and burns of the maximum uint256 amount revert.
• Permanent outcomes: tokens sent to the token contract itself are stuck for good. A fully burned token still rejects any transfer above zero. Unknown functions such as initialize, unpause and issue revert.
• Fuzz tests (1000 runs each): reverts above the allowance and above the balance, approve replacing the old value, chained transfers then a burn keeping totals consistent, and burning any holder's full balance.

I didn't write a .imd-findings.json, because there was nothing to report. One harmless quirk I noted but didn't file: transferFrom(address(0), x, 0) succeeds and emits Transfer(0, x, 0), which looks like a mint of zero. Standard ERC-20s commonly allow zero-value calls like this, so it isn't a defect.

The new files are not committed.

Review complete. The findings file is at .imd-findings.json with one finding and seven coverage rows.

Outcome. The MAD token's arithmetic is sound across the Math Precision, Boundary and Numerical Gap checklists. There is no division, no scale conversion, no downcast and no external call. Each of the three unchecked blocks sits behind a guard that bounds it, and the credit in _transfer is bounded by the sum-of-balances invariant. I found one low-severity boundary defect and nothing above it.

Finding (low). transferFrom(address(0), to, 0) succeeds from any caller and emits Transfer(0x0, to, 0), the event shape reserved for minting. The receiver and spender are checked against the zero address but the sender is not, and the zero-amount edge passes both the allowance and balance guards. No balance or supply changes. The proof test under test/scratch/ZeroSender.t.sol fails on the current code and is embedded in the findings file. The suggested fix is a sender check at the top of _transfer, which keeps the intended design.

What I verified, all passing.

• Constructor supply constant equals the manifest value, with 18 decimals.
• Self-transfer of the whole balance conserves, through both transfer and transferFrom.
• Max-uint and supply-plus-one amounts revert on transfer and burn; an unlimited allowance still requires balance; an allowance of max-minus-one decrements normally.
• A handler-driven invariant run of 128,000 random calls kept sum of balances equal to totalSupply, supply never above initial, and the zero address at zero balance.
• Reachable-opcode scan of the compiled runtime shows no DELEGATECALL, CALLCODE or SELFDESTRUCT, which is outside my area but cheap to confirm.

Leads dismissed. The aderyn large-literal note is stylistic only. Zero-amount transferFrom from an arbitrary holder without allowance succeeds, but OpenZeppelin behaves the same way and the standard permits it, so it is recorded in coverage rather than reported.

Coverage. All four listed entry points have rows: approve, burn and transfer hold, and transferFrom carries the finding. Nothing in my area was left unreached. Scratch tests remain under test/scratch/, which is discarded.

I've written the review to .imd-findings.json. It has one finding, rated low, and the token is otherwise sound.

Finding 1 (low): transferFrom accepts the zero address as the sender (src/MADToken.sol:113)

• Three specialists (permissions, flow and math) reported the same root cause, so I merged them into one finding.
• _transfer checks that the receiver isn't the zero address, but never checks the sender.
• Reproduction: anyone can call transferFrom(address(0), to, 0). The allowance check passes because 0 < 0 is false, and so does the balance check. The call succeeds and emits Transfer(0x0, to, 0), which is exactly what a mint event looks like.
• Impact: no balance or total supply changes, and any amount above zero reverts with InsufficientAllowance. The harm is limited to off-chain tools like block explorers and indexers, which would show fake mints on a token that promises nothing mints after deployment.
• Fix: add if (from == address(0)) revert InvalidSender(address(0)); at the top of _transfer, with a new custom error.
• Check: I ran both specialist proof tests against the current code and both fail as their findings describe. Because the finding is low, I didn't attach a proof to it.

Coverage:

Entry point	Verdict	Why
approve	holds	Sets the caller's allowance outright and rejects a zero spender
burn	holds	Only takes from the caller's own balance, after checking it
transfer	holds	Moves the exact amount with no fee; self-transfers work
transferFrom	finding 1	Allowance and balance handling are correct apart from the zero-sender case

I also checked these and found nothing wrong:

• Supply: there's no way to mint after the constructor, and no owner, pause or external calls.
• Manifest: launch.json states the supply as 1e27, which matches the constructor. Its empty constructor argument list matches the token's constructor, which takes none.
• Size: the deployed code is 1,676 bytes, well under the 24,576-byte limit.
• Tests: all 59 of the repository's existing tests pass.

The other two specialists reported nothing. The only static analysis lead, a large numeric literal at line 25, is just the supply constant and isn't a defect. I deleted my scratch test files, and the working tree has no changes.