Fuzzing + Formal Verification + Invariant Testing: Combining Them All

By alex

Here's a common mistake: teams pick one tool and treat it as their entire testing strategy. "We fuzz with Echidna" or "We verify with Certora." That's like saying "we test with unit tests" — it's a start, but it's leaving bugs on the table.

The real power comes from combining fuzzing, formal verification, and invariant testing into a single workflow. Each catches what the others miss. And with the right setup, you can write your properties once and run them across all three approaches.

Let's build that workflow.

What each approach catches (That others miss)

Before we combine anything, you need to understand the gaps.

Fuzzing finds

• Sequence-dependent bugs. Deposit, then price drop, then borrow, then liquidate — the fuzzer discovers these multi-step attack paths by trying millions of random sequences. FV can't easily reason about arbitrary-length sequences.
• Integration bugs. When contract A calls contract B which triggers a callback to contract A, the fuzzer runs the actual code. No modeling needed.
• Unexpected edge cases in real execution. Gas-related issues, stack depth problems, EVM-specific quirks, the fuzzer hits these because it runs real bytecode.

Formal verification finds

• Arithmetic boundary bugs. That one specific input value where a * b overflows? The fuzzer might never generate it. FV checks every possible value.
• Provable correctness. "This function is correct for ALL inputs" is a guarantee only FV can give. Fuzzing says "I tried a lot and it didn't break."
• Subtle invariant violations. If a rounding error only produces a wrong result for a narrow range of inputs, FV will identify that range exactly.

Invariant testing finds

• Stateful property violations. System-level invariants, solvency, supply consistency, access control, tested over sequences of real transactions.
• Ghost variable drift. Expected-value tracking catches accounting bugs that accumulate over many operations.
• Cross-contract consistency. Invariants that span multiple contracts catch bugs in the interfaces between them.

The overlap between these isn't as big as you'd think. In practice, I've seen protocols where fuzzing found 40% of the bugs, FV found 30%, and invariant testing caught the remaining 30%. Drop any one approach and you lose a chunk of coverage.

The unified property format

Here's the key insight: write properties once, test them three ways.

The Chimera framework makes this possible. You write properties as Solidity functions, and Chimera gives you adapters for Echidna, Medusa, and Foundry. For Halmos, you can write symbolic versions of the same properties.

Let's use a concrete example. Say you have a token vault with this critical property: depositing X assets should mint at least 1 share, and withdrawing all shares should return at least X assets minus fees.

The property in Chimera (for fuzzing)

// Properties.sol -- shared across all fuzzers
abstract contract Properties is TargetFunctions {

    function invariant_noZeroShareDeposits() public view returns (bool) {
        // After any deposit, the user must have received shares
        // (Checked via ghost tracking)
        for (uint256 i = 0; i < actors.length; i++) {
            if (ghost_deposited[actors[i]] > 0) {
                if (vault.balanceOf(actors[i]) == 0) {
                    return false;
                }
            }
        }
        return true;
    }

    function invariant_solvency() public view returns (bool) {
        // Vault's actual token balance must cover total assets
        return token.balanceOf(address(vault)) >= vault.totalAssets();
    }

    function invariant_supplyConsistency() public view returns (bool) {
        uint256 sum;
        for (uint256 i = 0; i < actors.length; i++) {
            sum += vault.balanceOf(actors[i]);
        }
        return sum == vault.totalSupply();
    }
}

These properties run on Echidna, Medusa, and Foundry without changes. Chimera handles the glue.

The same property in Halmos (for formal verification)

// FormalProperties.sol -- symbolic versions
contract FormalProperties is Test {
    Vault vault;
    MockERC20 token;

    function setUp() public {
        token = new MockERC20("Token", "TKN", 18);
        vault = new Vault(token);
        // Seed with initial liquidity to avoid first-depositor edge case
        token.mint(address(this), 1000e18);
        token.approve(address(vault), 1000e18);
        vault.deposit(1000e18, address(this));
    }

    function check_depositAlwaysMintsShares(uint256 assets) public {
        vm.assume(assets > 0);
        vm.assume(assets <= 1_000_000e18); // realistic bound

        address user = address(0xBEEF);
        token.mint(user, assets);

        vm.startPrank(user);
        token.approve(address(vault), assets);

        uint256 sharesBefore = vault.balanceOf(user);
        vault.deposit(assets, user);
        uint256 sharesAfter = vault.balanceOf(user);
        vm.stopPrank();

        // Must receive at least 1 share
        assert(sharesAfter > sharesBefore);
    }

    function check_withdrawNeverExceedsDeposit(uint256 assets) public {
        vm.assume(assets > 0);
        vm.assume(assets <= 1_000_000e18);

        address user = address(0xBEEF);
        token.mint(user, assets);

        vm.startPrank(user);
        token.approve(address(vault), assets);
        uint256 shares = vault.deposit(assets, user);

        uint256 balanceBefore = token.balanceOf(user);
        vault.redeem(shares, user, user);
        uint256 balanceAfter = token.balanceOf(user);
        vm.stopPrank();

        uint256 received = balanceAfter - balanceBefore;
        // Should get back at most what we deposited
        assert(received <= assets);
    }
}

Halmos checks these for every possible assets value (within the vm.assume constraints). If there's any amount where deposit returns zero shares, Halmos will find it and give you the exact value.

Running all three

# Fuzzing with Echidna (coverage-guided, sequence-aware)
echidna . --contract CryticTester --config echidna.yaml

# Fuzzing with Medusa (parallel, coverage-guided)
medusa fuzz --target-contracts MedusaTester

# Fuzzing with Foundry (fast iteration, CI-friendly)
forge test --match-contract FoundryTester

# Formal verification with Halmos (symbolic, proves for all inputs)
halmos --contract FormalProperties

Same properties. Four different engines. Each explores differently.

The practical workflow

Here's how this works in a real project:

Step 1: write properties first

Before writing any target functions or handlers, define what "correct" means. Start with the big ones:

• Solvency: The protocol can always pay out what it owes.
• Supply consistency: Sum of individual balances equals total supply.
• Access control: Only authorized addresses can call restricted functions.
• Monotonicity: Share price never decreases (excluding external yield changes).

Write these as Chimera-compatible properties.

Step 2: build the fuzzing harness

Add target functions (handlers) that wrap protocol interactions with proper input bounding and ghost variable tracking. This is where most of the work happens.

abstract contract TargetFunctions is Setup {
    // Ghost state
    uint256 ghost_totalDeposited;
    uint256 ghost_totalWithdrawn;
    mapping(address => uint256) ghost_userDeposited;

    function handler_deposit(uint256 actorSeed, uint256 amount) public {
        address actor = _getActor(actorSeed);
        amount = clampBetween(amount, 1, token.balanceOf(actor));

        vm.prank(actor);
        token.approve(address(vault), amount);
        vm.prank(actor);
        vault.deposit(amount, actor);

        ghost_totalDeposited += amount;
        ghost_userDeposited[actor] += amount;
    }

    function handler_withdraw(uint256 actorSeed, uint256 amount) public {
        address actor = _getActor(actorSeed);
        uint256 maxWithdraw = vault.maxWithdraw(actor);
        if (maxWithdraw == 0) return;
        amount = clampBetween(amount, 1, maxWithdraw);

        vm.prank(actor);
        vault.withdraw(amount, actor, actor);

        ghost_totalWithdrawn += amount;
    }
}

Step 3: run fuzzing campaigns

Run short campaigns during development (Foundry in CI). Run long campaigns before audits (Echidna/Medusa overnight).

# echidna.yaml
testMode: "assertion"
testLimit: 500000
seqLen: 100
corpusDir: "corpus"

Step 4: write formal specs for critical functions

Take your most critical properties and write Halmos versions. Focus on:

• Math libraries (fixed-point arithmetic, share conversion)
• Fee calculations
• Access control checks
• Token minting/burning bounds

Don't try to formally verify everything. It's too expensive. Pick the 20% of code where mathematical certainty matters most.

Step 5: run both in CI

# .github/workflows/security.yml
jobs:
  fuzz:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Run Foundry invariant tests
        run: forge test --match-contract InvariantTest
      - name: Run Echidna (short campaign)
        run: echidna . --contract CryticTester --config echidna-ci.yaml

  formal:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Run Halmos
        run: halmos --contract FormalProperties --loop 5

Fuzzing is your fast feedback loop. FV is your confidence check.

Decision matrix: which approach for which bug class

Bug Class	Fuzzing	FV	Invariant Testing
Arithmetic overflow	Medium	High	Low
Rounding errors (single-call)	Medium	High	Medium
Rounding errors (accumulated)	High	Low	High
Reentrancy	High	Low	Medium
Access control bypass	Medium	High	Medium
Oracle manipulation	High	Low	High
Flash loan attacks	High	Low	High
Share inflation / first depositor	Medium	High	High
Accounting drift over time	High	Low	High
Incorrect fee calculation	Medium	High	Medium
Liquidation edge cases	High	Low	High
Governance manipulation	High	Low	Medium
Cross-contract state corruption	High	Low	High

Read this table carefully. Notice the pattern: fuzzing and invariant testing are strong on stateful, sequence-dependent bugs. FV is strong on single-function correctness and arithmetic. The combination covers nearly everything.

A real example: testing a fee mechanism

Let's say your vault charges a 0.3% management fee, calculated annually and accrued per block. Here's how each approach tests it:

Fuzzing: Run thousands of deposit/withdraw/accrue sequences. The ghost variable tracks expected fees. If the actual accrued fees ever diverge from expected, the invariant fails. This catches bugs where the fee calculation is wrong in specific states, like when total supply is very small or very large.

function handler_accruesFees() public {
    uint256 elapsed = clampBetween(block.timestamp, 1, 365 days);
    vm.warp(block.timestamp + elapsed);

    uint256 expectedFee = vault.totalAssets() * 30 * elapsed / (10000 * 365 days);
    ghost_expectedFees += expectedFee;

    vault.accrueManagementFee();
}

function invariant_feesAccurate() public view returns (bool) {
    // Allow 0.1% tolerance for rounding
    uint256 actualFees = vault.accruedFees();
    uint256 tolerance = ghost_expectedFees / 1000;
    return actualFees >= ghost_expectedFees - tolerance
        && actualFees <= ghost_expectedFees + tolerance;
}

FV: Prove that for any totalAssets, elapsed, and feeRate, the fee calculation doesn't overflow and produces the correct result. This catches the case where totalAssets * feeRate * elapsed overflows for large values.

function check_feeCalculationNoOverflow(uint256 totalAssets, uint256 elapsed) public {
    vm.assume(totalAssets > 0 && totalAssets <= 1e30);
    vm.assume(elapsed > 0 && elapsed <= 365 days);

    // This should never overflow
    uint256 fee = totalAssets * 30 * elapsed / (10000 * 365 days);

    // Fee should be less than total assets
    assert(fee < totalAssets);

    // Fee should be proportional to time
    assert(fee > 0);
}

Invariant testing: The system-level invariant checks that total fees collected plus total user withdrawals plus remaining balances equals total deposits plus yield. This catches scenarios where fees are double-counted or missed entirely.

Together, these three approaches cover: the math is correct (FV), the implementation matches the math in all states (fuzzing), and the accounting is consistent end-to-end (invariant testing).

Common pitfalls when combining

Don't duplicate effort. If Halmos already proved a function is correct for all inputs, you don't need the fuzzer to spend cycles on the same function. Focus fuzzing on the stateful, multi-contract stuff.

Keep specs in sync. If you update a property in your fuzzing suite, update the Halmos version too. Stale specs are worse than no specs, they give false confidence.

Don't over-model in FV. The temptation with formal verification is to model everything precisely. Resist it. Model what you need, assume the rest. A verified subset is better than an incomplete verification that times out.

Share test infrastructure. Your fuzzing setup (mock contracts, deployment scripts, actor helpers) can be reused for FV tests. Don't build two separate test worlds.

Getting started

If you're starting from scratch, here's the order:

1. Write invariant tests with the Chimera framework. Get them running on Foundry first.
2. Add Echidna or Medusa for deeper fuzzing campaigns.
3. Pick your critical math functions and add Halmos specs.
4. Set up CI to run all of them.

This isn't a weekend project. But it's the difference between "we tested our protocol" and "we know our protocol is correct." And in DeFi, that difference is measured in millions of dollars.

For specific tool comparisons, check out Echidna vs Medusa, Halmos Symbolic Execution Guide, and Fuzzing vs Formal Verification.

Get a Security Review

---

alex leads security strategy at Recon. He's built combined fuzzing + FV pipelines for protocols holding hundreds of millions in TVL and still finds new ways to break things every week.