Implemented Ponziramid (PONZI): 1 billion tokens, 18 decimals, minted once to the deployer.

Included vendored dependencies, deployment documentation, and success, failure, fuzz, and invariant tests.

Verified with Solidity 0.8.26:

• forge build passed.
• forge test: 38 results passed.
• forge fmt --check passed.
• Clean offline checks with an empty environment passed.

The separate protected launch harness remains for the independent verifier.

Created launch.json matching Ponziramid’s constructor, exact supply, required pool settings, and verbatim economics.

forge build succeeded; forge test passed all 38 tests. Manifest fields and constructor ABI checks passed. Only launch.json is changed for submission.

The review is complete. The findings file is written with an empty list and a full coverage record, and the tree is unchanged apart from that file.

Result: no defects found. Ponziramid is an unmodified OpenZeppelin 5.4.0 ERC-20 with a single constructor mint, and every failure mode in the Execution Trace, Periphery and First Principles guides was checked against it without finding a reachable defect.

What I verified, by area:

• Execution Trace. Traced approve, transfer and transferFrom from entry to storage. Zero-address sender, recipient and spender revert. Balance and allowance checks precede the unchecked arithmetic they guard. Finite allowances are consumed exactly, with no residual, and the max allowance is preserved. Failed calls roll back atomically. There are no sentinel paths, external calls, callbacks or stale reads.
• Periphery. All five vendored OpenZeppelin files are byte-identical to the pinned upstream commit for v5.4.0. The Context base is the plain one, so the spender is always the real caller. An opcode scan of the runtime found no CALL, STATICCALL, CREATE, DELEGATECALL, CALLCODE or SELFDESTRUCT, so the token has no reentrancy or dependency surface.
• First Principles. The supply constant is exactly 10^27, which closes the aderyn large-literal lead. The mint goes to the immediate deployer, so a CREATE2 factory holds everything and the wallet calling it holds nothing. No public or external function can mint, burn, pause, freeze or seize. There is no payable entry point.

I ran the full existing suite and a scratch test of my own covering the factory mint, the 10/80/10 launch split, allowance edge cases and the opcode scan. All passed. The scratch test was removed afterwards.

One limit on coverage: the Uniswap v4 seed and swap flow could not be executed locally because v4-core is not vendored. The token side of that flow is plain and verified; the pool interaction itself is left to the verifier's protected harness, and the coverage record says so.

The review is complete. The findings file is written with an empty findings list and full coverage, and the scratch tests are removed so the working tree holds only the review output.

Result: no defects found in the Math Precision, Boundary or Numerical Gap area.

What I checked:

• The only production contract is a 16-line fixed-supply token over OpenZeppelin 5.4.0. It mints 10^27 units once to the deployer and adds no arithmetic of its own.
• Vendored dependency integrity. All five vendored OpenZeppelin files are byte-identical to the upstream v5.4.0 commit, so the inherited transfer and allowance math is the audited upstream code.
• Math Precision guide. There are no divisions, no downcasts, no decimal conversions and no fee formulas. The unchecked blocks in the inherited balance update are sound because every balance is bounded by the constructor-only supply. The allowance decrement is guarded by an explicit insufficient-allowance revert before the unchecked subtraction.
• Boundary guide. The token makes no external calls, has no payable path, decodes no bytes, and its only sentinel branches are the zero-address rejections. Both sides of each were traced. Zero, one wei, exact balance, balance plus one and max uint were exercised on every entry point.
• Numerical Gap guide. Supply conservation holds under zero-value fast paths and under fuzzed splits. The launch shares of ten and eighty percent divide the supply with no remainder, and the whole supply fits in the uint128 and int128 types the Uniswap v4 seed path uses.
• Static analysis lead. The aderyn large-literal note points at a compile-time constant that evaluates exactly to 10^27. It is not a defect.

Verification run: the delivered suite of 38 tests passed, and my 8 scratch tests covering the corners above passed before I deleted them.

Coverage in .imd-findings.json has one row for each of the three listed entry points plus four invariant rows, all marked holds.

The findings file validates, the quoted snippet matches line 8 of the token, the scratch directory is removed, and git status shows only the untracked findings file. The review is complete.

Outcome: no exploitable defect in the Ponziramid token. One informational finding is recorded in .imd-findings.json with a concrete reproduction and seven coverage rows.

What was checked

• The token is OpenZeppelin 5.4.0 ERC20 with a single constructor mint of 10^27 units to the deployer. All six vendored OpenZeppelin files diffed byte-identical to upstream v5.4.0, so the inherited behaviour is the audited library's.
• Economic Security guide: no external dependencies, oracles, callbacks, hooks, permit, proxy, admin, pause, blacklist, fee, or rebase. Nothing can be extracted, frozen, or diluted. Decimals return 18 as the brief requires.
• Invariant guide: supply is fixed at construction with no mint or burn path in the ABI. Balance sum equals supply through the single OpenZeppelin update function. Allowances are consumed exactly and the infinite allowance is preserved.
• Flow Gap guide: transfers return true and move exact amounts, so the factory to distributor, claim, single-sided seed, and buy and sell flows in the protected harness arrive whole. No launch manifest exists yet, which is expected before the manifest step.
• The repo suite of 38 tests, including the stateful invariant runs, passes on Foundry 1.8.3 with Solidity 0.8.26. The aderyn large-literal note is the correct supply constant and not a defect.

The one finding, severity info: a zero-value transferFrom from any holder succeeds without an allowance and emits a Transfer attributed to that holder. This is ERC-20 compliant, is OpenZeppelin's default, and the author's own test marks it as intended. It moves no funds. Its only effect is the off-chain address-poisoning pattern, so I reported it with a reproduction and an optional override rather than as a blocking defect.

Coverage: approve and transfer hold, transferFrom carries the informational finding, and the three invariant and flow rows hold. Nothing in the assigned area was left unreached.

The review is complete and the findings file is written. The working tree is clean apart from the untracked findings file (git status reported no tracked changes).

Result: no defects found in the Access Control, Trust Gap and Asymmetry area. The findings file holds an empty list and a nine-row coverage record, all holds.

What I checked:

• Permission model. The contract is OpenZeppelin ERC20 v5.4.0 plus a constructor that mints the fixed supply to msg.sender. The compiled ABI has only the standard ERC-20 functions and one constant getter. There is no owner, initializer, proxy, pause, blacklist, mint, burn, rescue, or payable entry. Unknown selectors and ETH sends revert.
• Inconsistent guards. Balances are written only through the transfer path, which debits msg.sender or an address that granted an allowance to msg.sender. Allowances are written only by the caller's own row. A scratch test confirmed the deployer, a stranger, and the holder itself all fail transferFrom at zero allowance.
• Asymmetry. transfer and transferFrom produce identical balance deltas across 512 fuzz runs. Finite allowances decrement, the max allowance stays unlimited, and both remain bounded by the sender's balance. Mint and burn branches in the base are unreachable after construction.
• Trust gap. No privileged actor exists, so no access-times-economics seam applies. The only asymmetric position is the initial holder, which is the factory by construction and matches the protected launch test.
• Supply chain. The five vendored OpenZeppelin files hash byte-for-byte to the pinned upstream commit. The runtime bytecode contains no call, create, delegatecall, callcode or selfdestruct opcodes.
• Static-analysis lead. The aderyn large-literal note is the supply constant, which equals the manifest total supply. Not a defect.

The existing 38-test suite passes. The scratch probe I used for evidence passed all seven tests and has been deleted, as test/scratch is not kept.

Expanded tests under test/ with failure paths, allowance boundaries, fuzz properties, and stateful invariants.

Validation passed:

• forge build
• forge test: 49 passed
• 32,768 invariant-handler calls

No implementation defects found. Only two test files changed.

I found no defects in Ponziramid and wrote an empty findings list to .imd-findings.json. I traced the code and didn't run any tests.

• The contract: src/Ponziramid.sol is OpenZeppelin's standard ERC20 with nothing changed. Its constructor takes no arguments and mints 1e27 (one billion tokens at 18 decimals) once to msg.sender, which is the factory. It has no admin roles, no way to mint more later, and no fee or burn on transfer, so the launch transfers move exact amounts.
• The manifest: launch.json matches the contract. The constructor has no parameters and constructorArgs is empty, totalSupply is 1e27 and decimals is 18. The contract is small, so the size limits don't apply.
• Specialist finding (dropped): The one specialist finding, from economics, was info level: anyone can call transferFrom(victim, x, 0) without an allowance and it emits a Transfer event. I dropped it because standard ERC-20 allows this and it changes no balance or allowance.
• Static analysis: The aderyn "large numeric literal" note is about the supply constant. It's a style point, not a defect.
• Coverage: I marked all three entry points (approve, transfer, transferFrom) as holds.