Smart Contract Audits: Finding What Compiler Misses

Euler Finance March 2023: $197M lost via flash loan on donateToReserves. Contract passed multiple audits. Vulnerability existed over a year. Auditors checked the function, missed it violated health factor invariant when combined with liquidate. Normal for complex DeFi: vulnerability isn't function bug, but invariant violation across call chains.

What Static Analysis Misses

Slither finds reentrancy, overflow, tx.origin misuse, variable shadowing. Real projects: dozens of warnings, 0-2 critical. Rest is noise. Won't find logical vulnerabilities.

Mythril uses symbolic execution. On 20-contract protocol with cross-contract calls — path explosion, hangs or false positives.

Both mandatory first pass. Don't replace manual analysis.

Fuzzing: Where Echidna and Foundry Find Real Bugs

Echidna — property-based fuzzer. Define invariants as Solidity functions, Echidna generates random sequences trying to break them.

Real: lending protocol, Echidna found deposit → borrow → liquidate → repay sequence violating totalAssets() >= totalLiabilities(). Humans wouldn't construct this.

Foundry fuzzing simpler to integrate. Stateful via invariant tests. Real project: vault contract, Foundry fuzz found maxWithdraw returning > actual balance at specific ratio. Hardhat unit tests missed it.

Medusa (Trail of Bits) supports corpus-guided fuzzing, faster on large contracts.

Formal Verification: When Needed

Formal verification proves contract satisfies spec for ALL inputs — not N random, but mathematically all. Certora Prover, K Framework, Halmos.

MakerDAO, Aave, Uniswap use Certora in CI/CD — each PR auto-verified.

Limitations: unbounded loops, hash functions, signature verification. For simple math (AMM, lending) works great.

Makes sense for contracts managing > $50M, updated rarely, with clearly formalizable invariants.

Attack Vectors Junior Auditors Miss

Storage collision in proxy. If implementation declares variable in slot 0 overlapping proxy storage — silent override.

Read-only reentrancy. External contract reads state via view during reentrancy-vulnerable moment — guard doesn't help. Curve pools 2023.

Oracle manipulation via TWAP. Harder than spot, but possible on low-liquidity pairs.

Gas griefing on loops. Attacker adds thousands of zero-balance addresses — function inaccessible.

Front-running on MEV. Use minAmountOut / deadline and checks.

Complete Audit Structure

Phase 1 — automated (1-2 days): Slither, Mythril, Aderyn. Triage.

Phase 2 — manual (5-15 days): line-by-line. Focus: external/public functions, all transfer/call/delegatecall, state changes before checks.

Phase 3 — fuzzing (2-5 days): Echidna/Foundry invariant tests. Fork mainnet.

Phase 4 — report: severity (Critical/High/Medium/Low/Info) with PoC for Critical/High. Re-audit fixes.

Audit in CI/CD

Slither and Aderyn on every PR. Certora Prover on merge. Not replacement for full audit, but catches regressions.

Timelines

Simple token/NFT: 3-5 days. DeFi: 2-4 weeks. Full: 4-8 weeks. Re-audit: 3-7 days.

Save audit budget exactly once: before first hack.