DEV Community

ohmygod
ohmygod

Posted on

Halmos + Foundry: How Symbolic Testing Catches the Bugs Your Fuzzer Will Never Find

#security #solidity #defi #ethereum

Smart contract fuzzing has become table stakes for security-conscious teams. Tools like Echidna, Medusa, and Foundry's built-in fuzzer catch a remarkable range of bugs. But fuzzing has a fundamental limitation: it explores random paths through an astronomical state space, hoping to stumble on the one sequence that triggers a vulnerability.

What if the bug requires a specific 256-bit input that a random search will statistically never produce?

Enter Halmos — a16z crypto's open-source symbolic testing tool that turns your existing Foundry tests into formal verification specifications. Instead of testing with random inputs, Halmos tests with all possible inputs simultaneously by converting your contract logic into mathematical constraints and feeding them to an SMT solver.

This article walks through practical Halmos usage: from installation to writing symbolic tests that would have caught real exploits that fuzzing missed.

Why Fuzzing Isn't Enough: A Real Example

Consider the Alkemi protocol exploit from March 2026 ($89K lost). The vulnerability was a self-liquidation accounting error — a specific sequence where a user could be both liquidator and liquidatee simultaneously, extracting profit through a rounding discrepancy.

A fuzzer might eventually stumble on this sequence. But the probability of generating exactly the right combination of:

  1. A position at precisely the right collateral ratio
  2. A self-liquidation call with the exact parameters that trigger the rounding error
  3. The correct ordering of oracle updates

...is astronomically low. A symbolic execution tool mathematically proves whether such a path exists — or proves it doesn't.

Setting Up Halmos With Foundry

Halmos integrates directly into existing Foundry projects:

# Install Halmos
pip install halmos

# Verify installation
halmos --version

# Run symbolic tests (convention: prefix with check_)
halmos --contract MyContractTest
Enter fullscreen mode Exit fullscreen mode

The key insight: Halmos reuses your Foundry test structure. If you already have unit tests, you're halfway to formal verification.

Writing Your First Symbolic Test

Here's a standard Foundry fuzz test for an ERC-20 transfer:

function testFuzz_transfer(address to, uint256 amount) public {
    vm.assume(to != address(0));
    vm.assume(amount <= token.balanceOf(address(this)));

    uint256 senderBefore = token.balanceOf(address(this));
    uint256 receiverBefore = token.balanceOf(to);

    token.transfer(to, amount);

    assertEq(token.balanceOf(address(this)), senderBefore - amount);
    assertEq(token.balanceOf(to), receiverBefore + amount);
}
Enter fullscreen mode Exit fullscreen mode

Now here's the Halmos symbolic equivalent:

function check_transfer(address to, uint256 amount) public {
    // No vm.assume needed — Halmos explores ALL paths
    // including to == address(0) and amount > balance

    vm.assume(to != address(this)); // Avoid self-transfer edge case

    uint256 senderBefore = token.balanceOf(address(this));
    uint256 receiverBefore = token.balanceOf(to);
    uint256 totalBefore = senderBefore + receiverBefore;

    // Try the transfer — may revert, which is fine
    (bool success,) = address(token).call(
        abi.encodeCall(token.transfer, (to, amount))
    );

    if (success) {
        uint256 senderAfter = token.balanceOf(address(this));
        uint256 receiverAfter = token.balanceOf(to);

        // Conservation of value — the critical invariant
        assertEq(senderAfter + receiverAfter, totalBefore);

        // No negative balance
        assertGe(senderAfter, 0);
    }
}
Enter fullscreen mode Exit fullscreen mode

The check_ prefix tells Halmos to use symbolic execution. Every uint256 parameter becomes a symbolic variable representing all possible 256-bit values simultaneously.

Stateful Invariant Testing With Halmos v0.3.0

The July 2025 release of Halmos v0.3.0 introduced stateful invariant testing — the ability to explore sequences of function calls, not just single transactions. This is where Halmos truly outshines fuzzing for complex DeFi protocols.

contract LendingInvariantTest is Test {
    LendingPool pool;
    MockOracle oracle;

    function setUp() public {
        pool = new LendingPool();
        oracle = new MockOracle();
        pool.setOracle(address(oracle));
    }

    // Halmos will call these in arbitrary sequences
    function deposit(uint256 amount) public {
        amount = bound(amount, 1, 1e24);
        deal(address(token), address(this), amount);
        token.approve(address(pool), amount);
        pool.deposit(amount);
    }

    function borrow(uint256 amount) public {
        amount = bound(amount, 1, pool.availableLiquidity());
        pool.borrow(amount);
    }

    function updatePrice(uint256 price) public {
        price = bound(price, 1e6, 1e12);
        oracle.setPrice(price);
    }

    // THE INVARIANT: total deposits >= total borrows
    function invariant_solvency() public {
        assertGe(
            pool.totalDeposits(),
            pool.totalBorrows(),
            "Protocol became insolvent"
        );
    }
}
Enter fullscreen mode Exit fullscreen mode

The Pectra Precedent: Formal Verification in Production

a16z demonstrated Halmos's production capability by formally verifying the Ethereum Pectra hardfork system contracts (EIP-2935, EIP-7002, EIP-7251). These contracts are written in raw assembly for gas efficiency — the kind of code where a single off-by-one error could compromise the entire network.

The process:

  1. Translate EIP specifications into Solidity test assertions
  2. Run Halmos against the compiled assembly bytecode
  3. Prove that the bytecode matches spec for ALL possible inputs

This is the gold standard: mathematical proof that code does what the spec says.

Practical Workflow: Combining Fuzzing + Symbolic Testing

The optimal audit pipeline uses both approaches:

Security Testing Pipeline
─────────────────────────
1. Static Analysis (Slither, Aderyn)
   → Catch known patterns instantly

2. Unit Tests (Foundry)
   → Verify expected behavior

3. Fuzz Testing (Foundry/Echidna/Medusa)
   → Explore random states (fast, broad)

4. Symbolic Testing (Halmos)
   → Prove invariants (slow, complete)

5. Mutation Testing (slither-mutate)
   → Verify test quality itself
Enter fullscreen mode Exit fullscreen mode

When to use fuzzing: Broad exploration, quick feedback loops, complex multi-contract interactions where state explosion makes symbolic execution impractical.

When to use Halmos: Critical invariants (solvency, access control, arithmetic correctness), functions with large input spaces, assembly/Yul code.

Five Invariants Every DeFi Protocol Should Formally Verify

Based on Q1 2026 exploits, these are the invariants that would have prevented the most damage:

1. Conservation of Value 

function check_noValueCreation(uint256 amount, address user) public {
    uint256 totalBefore = token.totalSupply();
    // ... perform any protocol action ...
    uint256 totalAfter = token.totalSupply();
    assertEq(totalBefore, totalAfter, "Value created from nothing");
}
Enter fullscreen mode Exit fullscreen mode

Would have caught: Resolv USR minting ($25M), Solv double-mint

2. Access Control Completeness 

function check_onlyAuthorized(address caller, bytes4 selector) public {
    vm.assume(!protocol.hasRole(ADMIN_ROLE, caller));
    vm.prank(caller);
    (bool success,) = address(protocol).call(
        abi.encodePacked(selector)
    );
    assertFalse(success, "Unauthorized access succeeded");
}
Enter fullscreen mode Exit fullscreen mode

Would have caught: Step Finance key compromise impact

3. Oracle Freshness 

function check_oracleNotStale(uint256 timestamp) public {
    vm.warp(timestamp);
    uint256 price = oracle.getPrice();
    uint256 lastUpdate = oracle.lastUpdateTime();
    assertLe(
        timestamp - lastUpdate, MAX_STALENESS,
        "Stale oracle used in calculation"
    );
}
Enter fullscreen mode Exit fullscreen mode

Would have caught: Aave CAPO oracle desync ($26M wrongful liquidations)

4. No Self-Interaction Profit 

function check_noSelfLiquidationProfit(
    uint256 collateral, uint256 debt, uint256 price
) public {
    uint256 valueBefore = getAccountValue(address(this));
    pool.liquidate(address(this), debt);
    uint256 valueAfter = getAccountValue(address(this));
    assertLe(valueAfter, valueBefore, "Self-liquidation was profitable");
}
Enter fullscreen mode Exit fullscreen mode

Would have caught: Alkemi self-liquidation ($89K)

5. Withdrawal Completeness 

function check_fullWithdrawal(uint256 depositAmount) public {
    pool.deposit(depositAmount);
    uint256 shares = pool.balanceOf(address(this));
    pool.withdraw(shares);
    assertGe(
        token.balanceOf(address(this)), depositAmount,
        "Lost funds on deposit-withdraw cycle"
    );
}
Enter fullscreen mode Exit fullscreen mode

Would have caught: Venus donation attack rounding ($3.7M)

Halmos Limitations and Workarounds

Halmos isn't magic. Key limitations:

  1. Path explosion: Complex contracts with many branches can timeout. Use --loop 3 to bound loop iterations and --depth to limit call depth.

  2. External calls: Halmos can't reason about external contract state. Mock external dependencies explicitly.

  3. Storage-heavy contracts: Large storage layouts slow the SMT solver. Focus symbolic tests on critical paths.

  4. Time: A single check_ function might take minutes to hours. Run Halmos in CI nightly, not on every commit.

# Practical CI configuration
halmos --contract CriticalInvariants \
       --loop 3 \
       --depth 10 \
       --timeout 3600 \
       --solver-timeout-assertion 300
Enter fullscreen mode Exit fullscreen mode

Getting Started Today

  1. Pick one invariant. Start with conservation of value — it's the easiest to specify and catches the most exploits.

  2. Write a check_ test. Reuse your existing Foundry test structure. Change the prefix, remove vm.assume bounds, add assertions.

  3. Run Halmos. If it passes, you have mathematical proof. If it finds a counterexample, you found a bug before an attacker did.

  4. Iterate. Add invariants one at a time. Focus on the properties that, if violated, would mean protocol insolvency.

The DeFi industry lost $137M in Q1 2026. Most of these exploits violated simple, formalizable invariants. Fuzzing is necessary but not sufficient. Symbolic testing with Halmos closes the gap between "probably safe" and "provably safe."

This article is part of the DeFi Security Research series. Code examples are simplified for clarity — production implementations should include additional edge cases and gas considerations.

Top comments (0)