How an audit actually works: tools, tests, and threat modeling

An audit is not a stamp of approval

Picture a team that ships a lending protocol on Monday. By Friday, $300M has flowed in. They commissioned an audit, and the 40-page PDF sits on their website like a seal of safety. Here is the uncomfortable truth: that report is a snapshot of one specific commit hash, reviewed for a few weeks by humans who did not write the code, who could not test every path, and who were honest enough to say so on page one. A smart-contract audit reduces risk. It never removes it.

The clearest proof is Euler Finance. By March 2023 its code had been reviewed by roughly ten different audit engagements. It still lost about $197M to a single missing line: a `donateToReserves` function that never re-checked the donor's health factor, letting an attacker push their own account underwater and then self-liquidate at a profit. (Unusually, the attacker later returned almost all the funds.) Heavily audited, still drained. Treat every audit as defense in depth, not a guarantee.

So what does a real engagement look like? It is a pipeline, and each stage catches a different class of bug. The earlier rungs taught you the bug classes — reentrancy, overflow, broken access control, oracle manipulation. This rung's finale is the discipline that hunts them systematically.

1. Scope and threat model — fix the commit, list actors, assets, trust boundaries, and the invariants that must always hold.
2. Manual review + static analysis — read every line by hand, with Slither flagging known patterns as a backstop.
3. Tests and fuzzing — high-coverage unit tests for the cases you imagined, property fuzzing for the ones you didn't.
4. Formal verification — mathematically prove the few invariants whose violation would be catastrophic.
5. Report and remediation — write up findings with severity and a PoC, then re-review the fixes.
6. Bug bounty + monitoring — pay outsiders to keep attacking after launch, and watch the chain in real time.

Threat modeling: who attacks, what's at stake, what must always hold

Good auditors do not start by reading code. They start by drawing the system: actors (users, the admin/owner, keepers and liquidators, and the attacker), assets (the TVL, governance power, the price feed itself), and trust boundaries — every place attacker-controlled data crosses into your logic. The most important boundary is the one beginners ignore: every external call hands control to code you do not own.

Crucially, assume the attacker is rich. Thanks to flash loans, anyone can borrow tens of millions for the length of a single transaction, so "they would never have enough capital" is never a valid defense. Model the attacker as able to call your functions in any order, sandwich them with a front-run, and re-enter through any external call. Your threat model is the list of bad outcomes you are promising cannot happen.

That list becomes your invariants: properties that must be true after every possible sequence of calls, by anyone, forever. Invariants are the spine of modern auditing — both fuzzers and formal tools work by trying to violate them. Write them down before you touch the code. They are also the input to invariant testing later.

// Invariants for a yield vault — properties that must hold after ANY call.
// These are claims; the rest of the audit is an attempt to break them.

// 1. Conservation: shares are only created/destroyed by deposit/withdraw
//      sum(balanceOf[user] for all users) == totalSupply

// 2. Solvency: the vault always physically holds what it owes depositors
//      asset.balanceOf(vault) >= totalDeposited

// 3. Access: only the timelocked admin can pause or change parameters
//      msg.sender == admin  for setFee(), pause(), upgrade()

// 4. Monotonic share price: pricePerShare never decreases
//      except inside a documented, bounded loss event

// 5. No free money: every token leaving the vault is matched by an
//      equal-value token entering, within rounding tolerance

Manual review and static analysis with Slither

The heart of an audit is still a human reading every line with a suspicious mind. Static analysis is the backstop. Slither (from Trail of Bits) compiles your Solidity into an intermediate representation and runs dozens of detectors that recognize known-dangerous shapes: state written after an external call (a reentrancy smell), `tx.origin` used for auth, uninitialized storage, dangerous unchecked low-level calls, and arbitrary `delegatecall`. Under the hood it leans on taint analysis to track attacker-controlled data from an entry point to a sensitive sink.

$ slither src/Vault.sol

Reentrancy in Vault.withdraw(uint256) (src/Vault.sol#42-51):
    External calls:
    - (sent,) = msg.sender.call{value: amount}("")  (src/Vault.sol#47)
    State variables written after the call:
    - balances[msg.sender] = 0  (src/Vault.sol#49)   <-- effect AFTER interaction
    Reference: https://github.com/crytic/slither/wiki/Detector-Documentation#reentrancy

Vault.owner (src/Vault.sol#11) is never initialized — defaults to address(0).

INFO:Slither:src/Vault.sol analyzed (1 contract), 2 results found

Testing and fuzzing: from unit tests to invariant campaigns

Unit tests prove the cases you imagined. Fuzzing attacks the cases you didn't. A smart-contract fuzzer generates thousands of random inputs — and, in stateful mode, random sequences of calls with random arguments — then checks your invariants after each one. The instant a sequence breaks an invariant, it shrinks the counterexample to the smallest reproduction and hands it to you. This is the single highest-leverage technique an auditor has.

// Foundry invariant test. forge throws random call sequences at the
// vault (via the Handler) and asserts solvency after every single step.
contract VaultInvariants is StdInvariant, Test {
    Vault   vault;
    Handler handler;        // wraps deposit/withdraw with bounded inputs

    function setUp() public {
        vault   = new Vault(asset);
        handler = new Handler(vault);
        targetContract(address(handler));   // fuzz only through the handler
    }

    // INVARIANT #2: the vault can never owe more than it holds.
    function invariant_neverInsolvent() public view {
        assertGe(asset.balanceOf(address(vault)), vault.totalDeposited());
    }
}

// Echidna (Trail of Bits) writes properties IN Solidity. Any function
// prefixed echidna_ must return true no matter what the fuzzer calls.
contract TokenProps is MyToken {
    // INVARIANT #1: total supply always equals the sum of all balances.
    function echidna_supply_equals_balances() public view returns (bool) {
        return totalSupply() == _sumOfTrackedBalances();
    }
}
// $ echidna test/TokenProps.sol --contract TokenProps
// echidna_supply_equals_balances: PASSED  (50000 calls, 0 failures)

Tools like Foundry (forge) and Echidna are only as good as their handlers and bounds. If your handler lets the fuzzer deposit numbers that overflow before reaching real logic, or never approves tokens, the campaign explores garbage and reports a false "PASSED." Writing good handlers — realistic actors, sane input ranges, ghost variables that track expected state — is most of the skill. Honest auditors report their coverage, not just their green checkmarks.

Formal verification: proving, not just testing

Fuzzing samples the input space — millions of points, but still a finite slice of an effectively infinite space. Formal verification proves a property over all inputs at once. It feeds the contract and the invariant to an SMT solver via symbolic execution: instead of concrete numbers, variables become symbols, and the solver searches mathematically for any assignment that violates the rule. Tools: Certora Prover (with its CVL spec language), Halmos (symbolic Foundry tests), and Mythril/hevm.

// Certora CVL-style rule (illustrative): prove the solvency invariant
// holds after EVERY public method, for ALL inputs, with no counterexample.
rule neverInsolvent(method f) {
    // assume the invariant holds before the call
    require asset.balanceOf(currentContract) >= totalDeposited();

    env e; calldataarg args;
    f(e, args);                         // f = any function, args = any inputs

    // require it still holds afterward — the prover tries to falsify this
    assert asset.balanceOf(currentContract) >= totalDeposited();
}

Writing a finding: severity, PoC, and remediation

The deliverable is the finding. Each one is graded by severity, which combines impact (how bad if exploited — direct loss of funds is Critical; griefing or a stuck UI is Low) with likelihood (how easy to trigger — permissionless and atomic is high; needs the admin key is low). A clear finding states: a title, the severity and reasoning, the exact location and commit, a description, a concrete proof of concept, and a recommendation. A finding without a reproducible PoC is just an opinion.

[H-01] First-depositor inflation attack lets an attacker steal later deposits

Severity : High  (Impact: High — theft of user funds; Likelihood: Medium)
Target   : Vault.deposit() / convertToShares()   (commit a1b2c3d)

Description
  shares = assets * totalSupply / totalAssets.  When the pool is empty
  (totalSupply == 0) the first depositor mints 1 wei of shares, then sends
  a large amount of the underlying DIRECTLY to the vault (a donation that
  mints no shares). This inflates totalAssets, so the next depositor's
  shares = assets * 1 / totalAssets rounds DOWN to 0 — their assets are
  captured by the attacker's single share.

Proof of concept
  1. attacker.deposit(1 wei)        -> mints 1 share,  totalSupply = 1
  2. asset.transfer(vault, 10e18)   -> donation, no shares minted
  3. victim.deposit(5e18)           -> 5e18 * 1 / (10e18 + 1) = 0 shares
  4. attacker.redeem(1 share)       -> withdraws 15e18 + 1  (victim robbed)

Recommendation
  Use OpenZeppelin ERC4626's decimal-offset / virtual shares, OR seed the
  pool with a permanent dead-shares deposit at deployment, AND revert on
  zero-share mints:  require(shares > 0, "ZERO_SHARES");

This exact bug class lives in ERC-4626 vaults across DeFi, which is why OpenZeppelin baked virtual-shares mitigation into its standard implementation. After delivery comes the remediation round: the team fixes each finding, and the auditors re-review the patch — because fixes introduce bugs too. A finding is not closed until the fix itself has been verified against the same PoC.

Defense in depth: the audit is one slice of cheese

No single control stops every attack, so professionals stack them — the Swiss-cheese model: each layer has holes, but the holes rarely line up. The audit is one slice. Around it sit secure coding, tests, fuzzing, formal verification, more than one independent audit, a public bounty, and runtime defenses. An attacker now has to punch through all of them in the same place at the same time.

1. Secure coding — inherit audited OpenZeppelin libraries, follow checks-effects-interactions, keep the surface small.
2. Comprehensive tests + property fuzzing — high coverage plus invariant campaigns on every critical property.
3. Formal verification — prove the handful of invariants whose violation means insolvency.
4. One or more independent audits — different firms see different bugs; never rely on a single pair of eyes.
5. A public bug bounty — pay outsiders to keep attacking forever (Immunefi has paid white-hats up to $10M, e.g. the Wormhole critical).
6. Runtime defenses — monitoring/alerts, a pausable circuit breaker, a governance timelock, and TVL caps during gradual rollout.

Read enough post-mortems and the same lesson repeats: the master's mindset is adversarial humility. You assume your code is broken and spend your effort trying to prove it, knowing you will sometimes fail. An audit is not the moment you declare victory — it is one disciplined, honest slice in a defense that is never finished.