How audits, fuzzing and formal verification work

What an audit is, and what it is not

An audit is a small team reading a specific commit for a fixed number of engineer weeks, against a threat model, and writing down what they found. Its output is a list of findings ranked by severity, followed by a review of the fixes against a later commit. That is valuable and it is bounded: by time, by the scope the client defined, and by the reviewers' attention on the day.

Euler Finance is the standing example. Per Euler's own account, the donateToReserves function behind its March 2023 loss had been sent to audit, and the missing health check was not caught. Reviews reduce the probability of a bug; they cannot prove its absence. Proving absence, for a specific property, is what formal methods are for, and they have their own limits.

How a review runs

1. Freeze the scope

   A commit hash, the list of files in scope, documentation, and the assumptions the team relies on: trusted roles, supported tokens, oracle behavior. Anything not written down will not be reviewed.

2. Build the threat model

   Assets at risk, actors and their powers, trust boundaries, external dependencies, and the invariants the system must maintain. Good reviewers spend real time here, because every finding is a violation of something in this model.

3. Read, and prove suspicions with tests

   Line by line and flow by flow: every external call, every privileged path, every place value is computed. Suspected bugs become proof of concept tests, which is what separates a finding from a hunch.

4. Run the machines

   Static analysis on everything, fuzzing campaigns on the core logic, and sometimes symbolic or formal checks on the math that everything else depends on.

5. Report, fix, review the fixes

   Findings with severity and recommendations, then a second pass on the fix commit. Fixes introduce bugs often enough that this step is not optional.

Severity: impact times likelihood

Most firms rate a finding on two axes, how bad it is if exploited and how likely exploitation is, and combine them:

Bug bounty platforms define impact concretely, because money depends on it. Immunefi's classification system (version 2.3) treats direct theft of user funds, permanent freezing of funds, protocol insolvency and manipulation of governance results as critical; theft or freezing of unclaimed yield and temporary freezing as high; griefing and contracts unable to operate as medium; and failing to deliver promised returns without losing value as low. Reading the definitions tells you what a team considered in scope, which matters as much as the labels.

Static analysis: fast, shallow, always on

Static analysis reads code without running it and matches it against known bad shapes. The usual starting point is Slither from Trail of Bits, a Python framework for Solidity and Vyper that lifts code into its own intermediate representation, SlithIR, and runs about 100 built in detectors as of September 2026: reentrancy orderings, unchecked return values, uninitialized storage, dangerous DELEGATECALL, shadowed variables and many more.

It runs in seconds, so it belongs in CI on every commit. It also produces false positives, so the working pattern is to triage once, suppress with a comment explaining why, and fail the build on anything new. Its API lets a team encode its own rules, such as "every external function in this contract must carry this modifier", which turns a review checklist item into a check that never gets tired. What static analysis cannot see is meaning: whether a formula is right, whether a check belongs in this function, whether an incentive can be gamed.

Fuzzing and invariant testing

A fuzz test calls one function with many generated inputs. An invariant test, also called stateful fuzzing, calls random sequences of functions across a whole system and checks properties after every call. The second kind finds the bugs that matter, because real exploits are sequences: deposit, borrow, donate, liquidate.

In Foundry, invariant functions are named with the invariant_ prefix, and a handler contract wraps the system so the fuzzer calls it sensibly: bounding inputs, choosing among a few actors, and tracking "ghost" totals the system does not store. targetContract and targetSelector decide what gets called, and afterInvariant runs end of run checks.

// test/VaultInvariants.t.sol  (Foundry with forge-std; MockERC20 is any mock token with a public mint)
contract Handler is Test {
    ERC4626 public vault;
    MockERC20 public asset;
    uint256 public ghostIn;    // everything deposited or donated
    uint256 public ghostOut;   // everything redeemed
    bool public diluted;       // did any depositor lose value to an earlier actor?

    constructor(ERC4626 v, MockERC20 a) { vault = v; asset = a; }

    function _actor(uint256 seed) internal pure returns (address) {
        return address(uint160(0x10000 + bound(seed, 0, 4)));   // five users
    }

    function deposit(uint256 seed, uint256 amount) external {
        address user = _actor(seed);
        amount = bound(amount, 1, 1e30);
        asset.mint(user, amount);
        vm.startPrank(user);
        asset.approve(address(vault), amount);
        uint256 shares = vault.deposit(amount, user);
        vm.stopPrank();
        ghostIn += amount;
        uint256 back = vault.previewRedeem(shares);
        if (back + amount / 1000 + 1 < amount) diluted = true;  // lost more than 0.1% plus dust
    }

    function redeem(uint256 seed, uint256 shares) external {
        address user = _actor(seed);
        shares = bound(shares, 0, vault.balanceOf(user));
        if (shares == 0) return;
        vm.prank(user);
        ghostOut += vault.redeem(shares, user, user);
    }

    function donate(uint256 amount) external {   // anyone can send tokens directly
        amount = bound(amount, 0, 1e30);
        asset.mint(address(vault), amount);
        ghostIn += amount;
    }
}

contract VaultInvariants is Test {
    ERC4626 vault;
    MockERC20 asset;
    Handler handler;
    // setUp() deploys all three, then calls targetContract(address(handler));

    function invariant_solvent() public view {       // every share can be paid
        assertGe(asset.balanceOf(address(vault)),
                 vault.convertToAssets(vault.totalSupply()));
    }

    function invariant_noValueCreated() public view {  // sanity: never pays out more than it received
        assertLe(handler.ghostOut(), handler.ghostIn());
    }

    function invariant_depositsNotDiluted() public view {  // no depositor loses value to an earlier actor
        assertFalse(handler.diluted());
    }
}

// foundry.toml, set explicitly rather than relying on defaults:
// [invariant]
// runs = 256
// depth = 100
// fail_on_revert = false

The donate action is the important one. It encodes an ability every attacker has, sending tokens straight to a contract, which a happy path test suite never exercises. Against a naive vault, donate followed by deposit trips invariant_depositsNotDiluted. The aggregate invariants alone never fail on it, because the inflation attack moves value between users rather than creating it. Good invariants come in a few families:

• Solvency. Assets held cover every claim.
• Conservation. Nothing leaves that did not come in, fees aside.
• Monotonicity. A share price only falls through a defined loss event.
• Access. Only one role can change a given parameter.
• Liveness. A healthy user can always withdraw.

Two dedicated fuzzers go further than Foundry's built in engine. Echidna, from Trail of Bits and written in Haskell, is a property based fuzzer that generates call sequences from the contract ABI. Medusa, also from Trail of Bits, is written in Go on top of geth, with coverage guided and parallel fuzzing; version 1 was released on February 14, 2025, when Trail of Bits said its primary focus was shifting to Medusa while Echidna would continue to receive fixes. Coverage guidance is the key idea: inputs that reach new code are kept and mutated, so the campaign digs into rare states instead of retrying the obvious ones.

Symbolic execution: every input at once

A fuzzer samples inputs. A symbolic executor treats inputs as unknowns, follows every path through the code, and asks a constraint solver whether any assignment of the unknowns reaches a failing assertion. If one exists, it prints it as a concrete counterexample.

Halmos, from a16z, runs Foundry style tests symbolically. Test functions use the check_ prefix, every parameter stands for all values of its type, and vm.assume constrains them:

// Halmos runs a test symbolically: `assets` stands for every uint256 at once.
function check_roundTripNeverProfits(uint256 assets) public {
    vm.assume(assets > 0 && assets <= 1e30);
    asset.mint(address(this), assets);
    asset.approve(address(vault), assets);

    uint256 shares = vault.deposit(assets, address(this));
    uint256 out = vault.redeem(shares, address(this), address(this));

    assert(out <= assets);   // if this can fail, Halmos prints a concrete input that fails it
}

The honest limits: loops are unrolled only to a bound, the number of paths can explode in complex code, and Halmos reports assertion violations, not every revert, so an overflow you care about must be asserted explicitly. Within those bounds, "no counterexample" is a much stronger statement than "the fuzzer did not find one". Kontrol, from Runtime Verification, takes a similar Foundry first approach but proves tests against KEVM, a formal semantics of the EVM written in the K framework.

Formal verification, and what a proof proves

Formal verification proves that a property holds for all inputs and all states, not just those within a loop bound. A widely used prover built for smart contracts is the Certora Prover, which checks rules written in the Certora Verification Language. Certora made the Prover open source on February 24, 2025.

// Certora Verification Language. The Prover checks the rule for every
// input and every starting state, including states the protocol could never
// reach, which is why real specs add invariants that rule those out.
rule depositRedeemNeverProfits(uint256 assets) {
    env e;
    uint256 shares = deposit(e, assets, e.msg.sender);
    uint256 out    = redeem(e, shares, e.msg.sender, e.msg.sender);
    assert out <= assets, "round trip created value";
}

A proof is exactly as good as three things: the property, the model and the assumptions.

• The property. A prover proves what you wrote. "Nobody can withdraw more than their balance" says nothing about whether the balance was computed correctly. Weak specs produce true, useless proofs.
• Vacuity. If the assumptions rule out every state, every assertion passes. Provers offer sanity checks that flag rules which pass only because nothing satisfies their preconditions.
• The model. External calls to tokens, oracles and other protocols are usually summarized as well behaved. The proof holds for that idealized world.
• Outside the code. Oracle manipulation, governance capture and bad parameters are economic failures. Code can be proven correct and still be exploited through its inputs.

Competitive audits and bug bounties

Competitive audits invert the staffing model: instead of a small team for weeks, many independent researchers review the same code in a fixed window and are paid per valid, deduplicated finding. Code4rena, Sherlock and Cantina all run contests as of September 2026. Contests buy breadth and many perspectives; a dedicated team buys depth and continuity. Serious protocols often use both.

Bug bounties cover deployed code, indefinitely. Immunefi is a widely used platform for them, and one of its best known payouts is the $10 million Wormhole paid in 2022 for the uninitialized implementation described in the vulnerability classes guide, reported on February 24, 2022 and patched the same day with no funds lost. The design logic of a bounty is competitive: the reward has to be attractive next to what the bug could otherwise yield, after the cost and risk of laundering it.

For rescues during a live exploit, the Security Alliance (SEAL) publishes a Safe Harbor agreement that protocols adopt onchain in advance. SEAL's summary, as of September 2026, describes whitehats returning rescued funds within 72 hours for a bounty of 10% of recovered assets, capped at $1 million.

Monitoring and incident response

The same invariants you fuzz before launch can be watched after it. Balancer's post-mortem of its November 3, 2025 exploit gives a real timeline, all times UTC:

Twenty one minutes from first transaction to pause is fast. It still could not help the older pools, whose pause windows had expired by design. That is the real tradeoff behind emergency powers: a pause is protection for users and a power someone holds, and the right answer depends on who holds it and for how long (see admin keys and timelocks and governance design). A usable response plan has monitors on the invariants, alerting that wakes a person, pause and parameter transactions prepared in advance, a known path to SEAL 911 and exchanges, and someone who owns public communication.

How to read an audit report as a user

• Match the commit. The report names a commit hash. Check it against the verified source on the explorer, and check whether the contracts were upgraded after the report date.
• Read the scope. Were the oracle integration, the deployment scripts and the admin setup in it, or only the core contracts?
• Read the status of every finding. "Acknowledged" means not fixed. An acknowledged high is a live risk the team chose to accept.
• Look at the whole stack. Independent reviews, published invariant or formal verification work, a bounty sized sensibly against the value held, monitoring and a timelock on upgrades.
• Know the red flags. A report for a different version, an automated scan presented as an audit, a bounty that is trivial next to deposits, a large recent upgrade with no review.

Common questions

Where to go next