EVM Smart Contract Audit Checklist: Foundry to Certora

{"excerpt":"An EVM smart contract audit checklist covering Foundry fuzzing, Slither static analysis, and Certora formal verification for critical invariants.","tags":["Smart Contracts","EVM","Security Audit","Foundry","Certora"],"cover":"grid","content":"## Why one tool is never enough\n\nA single audit tool catches a fraction of the bugs that matter. Slither will flag reentrancy patterns and storage collisions in seconds, but it won't tell you that your liquidation math breaks when collateral price hits exactly zero. Foundry fuzzing will find that edge case if you write the invariant, but it can't prove your access control is airtight across every possible call sequence. Certora can prove that — but only if you spend the two or three days it takes to write correct specs. Real audits stack these tools in sequence, each one catching what the last one missed, and each one costing more engineering time than the last.\n\nThis is the workflow we run at TierZero for EVM trading bots and DeFi contracts before they touch mainnet. It's not exhaustive — no checklist is — but it's the order that finds the expensive bugs before the cheap ones waste your afternoon.\n\n## Stage 1: Static analysis with Slither (30 minutes to 2 hours)\n\nRun Slither first, always. It's free, it's fast, and it eliminates an entire class of noise before a human reads a single line.\n\nbash\nslither . --exclude-dependencies --filter-paths \"test|script\"\n\n\nOn a typical 15-contract DeFi protocol this surfaces 40-80 findings. Most are low severity — unused return values, missing zero-address checks, naming conventions. Triage them into a spreadsheet with three columns: finding, severity, dismissed-or-fixed. Don't skip the dismissal reasoning; six months later nobody remembers why unchecked was safe in that one loop.

The findings worth stopping for: reentrancy on external calls before state writes, delegatecall to untrusted addresses, and arithmetic that Slither flags as potentially overflowing outside unchecked blocks even on Solidity 0.8+. That last one surprises people — 0.8's built-in overflow checks don't save you from a uint256 that legitimately needs to wrap, or from a cast down to uint128 that silently truncates.\n\n## Stage 2: Foundry invariant and fuzz testing (2-5 days)\n\nStatic analysis proves nothing about behavior over time. Foundry's invariant testing does, by throwing random call sequences at your contract and checking that properties hold after every one.\n\nFor a trading bot's vault contract, the invariant that matters most is usually solvency: total shares outstanding should never let a withdrawal drain more than the vault's real balance.\n\nsolidity\nfunction invariant_solvency() public {\n uint256 totalAssets = vault.totalAssets();\n uint256 totalShares = vault.totalSupply();\n if (totalShares > 0) {\n assertGe(\n totalAssets,\n vault.convertToAssets(totalShares) - 1 // rounding slack\n );\n }\n}\n\n\nThe "- 1" rounding slack is deliberate — ERC4626-style vaults round in the protocol's favor by design, and an invariant that doesn't account for that will fail on day one for the wrong reason. Set runs to at least 1,000 and depth to 50+ in foundry.toml for anything handling real value; the default settings are tuned for speed, not coverage.\n\nFuzz your pricing and fee math separately from the invariant suite. Bounded fuzz tests on functions like calculateSlippage() or applyFundingRate() with bound() calls constraining inputs to realistic ranges catch off-by-one and rounding bugs that unit tests with three hardcoded values never will.\n\nExpect this stage to find 3-8 genuine issues on a mid-complexity protocol, and expect to spend more time writing good invariants than reading Foundry's output.\n\n## Stage 3: Manual review against known patterns (3-7 days)\n\nTooling won't catch business-logic errors — the ones where the code does exactly what it was written to do, and what it was written to do is wrong. This is where a senior reviewer walks the codebase against a pattern checklist:\n\n- Oracle manipulation: can a flash loan move the price feed your liquidation logic reads?\n- Access control drift: does every privileged function check the same role, or did someone forget onlyOwner on the new admin function added in commit #47?\n- Cross-function reentrancy: reentrancy guards on individual functions don't stop an attacker re-entering through a different function during the same call.\n- MEV exposure: can a searcher sandwich your swap() or front-run your liquidate() for guaranteed profit?\n- Upgrade safety: for proxy contracts, does the storage layout in v2 actually match v1's slot ordering?\n\nFor context on how this compares to non-EVM chains, our TON smart contract audit checklist for FunC and Tact covers the same manual-review discipline adapted to a very different execution model — TON's async message-passing breaks assumptions that hold on EVM.\n\n## Stage 4: Certora formal verification (3-10 days, invariants only)\n\nCertora isn't for the whole contract — that's not economical and it's not what the tool is good at. It's for the two or three invariants where a proof, not a test, is the only acceptable answer. Think: "total debt never exceeds total collateral value at any block," or "the sum of all user balances always equals total supply."\n\nWriting a CVL spec forces precision that fuzz testing doesn't:\n\n\nrule solvencyHolds(method f) {\n env e;\n calldataarg args;\n require totalAssets() >= totalLiabilities();\n f(e, args);\n assert totalAssets() >= totalLiabilities();\n}\n\n\nThis rule checks the property across every function in the contract, not just the ones you thought to test — Certora's prover explores the state space symbolically rather than sampling it. It routinely finds the one function nobody thought to invariant-test, usually an admin function or an emergency withdrawal path added late in development.\n\nThe catch: Certora requires a rules engineer who understands both your protocol and CVL syntax, and specs that are too loose prove nothing while specs that are too strict produce false counterexamples that eat a day of debugging. Budget for a specialist, not a generalist auditor learning CVL on your contract.\n\n## Putting it together\n\nOn a typical engagement this four-stage workflow runs 2-4 weeks depending on contract count and complexity, and costs scale accordingly — we break down realistic ranges by chain and scope in smart contract audit cost across EVM, Solana, and TON for 2026. If you're weighing whether your contract needs this level of rigor before you ship, read our take on when an audit is actually required before mainnet launch — the honest answer depends more on what the contract controls than on its line count.\n\nStatic analysis and fuzzing belong in every CI pipeline, not just the pre-launch audit — our code review and audit service sets that up as an ongoing gate rather than a one-time event, which is what most teams actually need once they start shipping upgrades.\n\nIf you're building the contract from scratch rather than auditing an existing one, get the review process involved during smart contract development, not after — fixing an invariant violation before mainnet is a code change, fixing it after is an incident.\n\nIf you want this workflow run against your contracts by people who write Certora specs for a living, talk to us about a smart contract audit."}