Halmos symbolic execution for smart contracts: setup, limitations, and when it beats fuzzing

Fuzzing and symbolic execution get lumped together as "advanced testing," but they solve the problem from opposite directions. A fuzzer throws random inputs at your code and hopes to trip over a bug. Symbolic execution doesn't guess — it treats inputs as mathematical variables and reasons about every possible path through the code. Halmos is the tool that brings symbolic execution to the Solidity world in a way that actually fits into existing Foundry workflows.

I've used Halmos alongside fuzzers on dozens of audits at Recon. It's not a replacement for fuzzing — it's a different lens. Here's how to set it up, where it shines, and where it falls apart.

What symbolic execution actually does

When you run a fuzzer like Echidna or Medusa, it generates concrete values — say, amount = 7291 — and checks if your property holds. It does this millions of times, sampling the input space randomly (or with coverage guidance). It's fast, but it can miss the one specific value that triggers a bug.

Symbolic execution doesn't pick values. Instead, it says "let amount be any possible uint256" and tracks how that symbolic value flows through every branch. At each conditional, it forks: one path where the condition is true, one where it's false. It then asks an SMT solver (like z3) whether any concrete value could make each path reach your assertion failure.

The upside: if a bug exists in the explored state space, symbolic execution will find it. No luck involved. The downside: the number of paths can explode exponentially, which is why this approach needs careful scoping.

Setting up Halmos

If you're already using Foundry, Halmos slots in with minimal friction. Install it:

pip install halmos

Halmos reads your Foundry project structure directly. You write test functions prefixed with check_ instead of test_, and Halmos treats every parameter as symbolic. Here's a minimal example — a property that works identically whether you run it with Foundry's fuzzer or with Halmos:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import "forge-std/Test.sol";
import "../src/SafeMath.sol";

contract SafeMathTest is Test {
    SafeMath internal math;

    function setUp() public {
        math = new SafeMath();
    }

    // Works with both: forge test and halmos
    function check_addDoesNotOverflow(uint128 a, uint128 b) public {
        uint256 result = math.safeAdd(a, b);
        assert(result >= a);
        assert(result >= b);
    }
}

Run it with Foundry's fuzzer:

forge test --match-test check_addDoesNotOverflow

Run it with Halmos:

halmos --function check_addDoesNotOverflow

Same property, two tools. Foundry will throw random uint128 pairs at it. Halmos will reason about all possible pairs symbolically.

Writing Halmos-specific properties

Where Halmos gets interesting is when you lean into symbolic reasoning. You can write properties that assert things about arbitrary storage states, not just function inputs:

function check_withdrawNeverExceedsBalance(uint256 depositAmt, uint256 withdrawAmt) public {
    // Symbolic setup: any deposit, then any withdrawal
    vm.assume(depositAmt > 0);
    vm.assume(withdrawAmt > 0);

    vault.deposit(depositAmt);

    uint256 balBefore = vault.balanceOf(address(this));

    // If withdraw doesn't revert, balance must decrease by exactly withdrawAmt
    try vault.withdraw(withdrawAmt) {
        uint256 balAfter = vault.balanceOf(address(this));
        assert(balBefore - balAfter == withdrawAmt);
    } catch {
        // Revert is acceptable — but only if withdrawAmt > balance
        assert(withdrawAmt > balBefore);
    }
}

Halmos will explore both the success and revert branches, and for each branch it'll ask: does any combination of depositAmt and withdrawAmt violate the assertion? If your vault has an off-by-one in the balance check, Halmos will hand you the exact counterexample.

Where Halmos finds bugs that fuzzers miss

Boundary conditions are where symbolic execution earns its keep. Consider a fee calculation:

function calculateFee(uint256 amount) public pure returns (uint256) {
    // Bug: integer division truncation means fee is 0 for amount < 1000
    return (amount * 3) / 1000;
}

function check_feeIsNonZeroForNonZeroAmount(uint256 amount) public {
    vm.assume(amount > 0);
    uint256 fee = calculateFee(amount);
    // This assertion should hold if we expect fees on all non-zero amounts
    assert(fee > 0);
}

A fuzzer sampling random uint256 values will almost never generate a value below 334 (the threshold where the fee rounds to zero). The probability is roughly 334 / 2^256 — essentially zero. Halmos will find amount = 1 as a counterexample instantly, because it doesn't sample — it solves.

This pattern shows up constantly in DeFi: rounding thresholds, precision boundaries, fee cliffs. These are exactly the bugs that slip through fuzzing campaigns but get caught by symbolic execution.

<a href="/request-audit" class="cta-button">Get multi-tool security testing</a>

Configuration and timeouts

Halmos has several flags you'll want to tune:

# Run with a 10-minute timeout per function, unroll loops up to 8 times
halmos --function check_ --loop 8 --solver-timeout-assertion 600000

# Target a specific contract
halmos --contract SafeMathTest --function check_addDoesNotOverflow

# Increase verbosity for debugging path explosion
halmos --function check_ --statistics --debug

# Set storage size limits to control memory usage
halmos --storage-layout solidity --solver-timeout-branching 10000

Key flags:

• --loop N: maximum loop unrolling depth (default is low, bump it for contracts with loops)
• --solver-timeout-assertion: milliseconds before the solver gives up on a single assertion
• --statistics: prints path counts and solver time — essential for understanding why a check is slow
• --solver-threads: parallelize solver queries if your machine has cores to spare

The limits: state space explosion

Halmos doesn't scale the way fuzzers do. Here's where it breaks down:

Loops. Every loop iteration forks the execution path. A for loop that runs up to 100 times creates 100 path branches at minimum. Halmos handles this with bounded unrolling (--loop N), but you're only verifying the property for loop counts up to N.

External calls. When your contract calls another contract, Halmos needs to reason about what that external contract might return. For known contracts it can inline the logic; for unknown ones, it has to assume the return value is symbolic, which multiplies paths further.

Stateful sequences. Halmos checks one function call at a time (or a short sequence you manually compose). It doesn't generate multi-transaction attack sequences the way a stateful fuzzer does. If the bug requires calling deposit(), then borrow(), then withdraw() in a specific order — that's fuzzer territory.

Large contracts. A contract with 50+ functions and deep inheritance chains will often time out. You'll need to isolate specific properties and test them against focused contract subsets.

Decision tree: Halmos vs fuzzing

Use this to pick the right tool for the job:

Reach for Halmos when:

• You're testing arithmetic properties (overflow, rounding, precision loss)
• The function under test has a small, bounded state space
• You need to prove a property holds for ALL inputs, not just sampled ones
• You're investigating a specific boundary condition or edge case
• The contract is small to medium-sized with limited external dependencies

Reach for fuzzing when:

• You're testing stateful invariants across multi-step transaction sequences
• The contract is large or has deep call chains to external protocols
• You're exploring behavior you don't fully understand yet (fuzzing as discovery)
• You need to test with realistic deployment scenarios (multiple actors, time progression)
• The property involves interactions between many contract functions

Use both when:

• You're doing a serious audit. Symbolic execution covers the boundary conditions fuzzers miss. Fuzzers cover the stateful sequences symbolic execution can't reach. They're complementary, not competing.

At Recon, we run Halmos checks alongside Echidna and Medusa campaigns as standard practice. The bugs each tool catches barely overlap — which is exactly why you want both in your pipeline.

For a deeper dive into fuzzing tool selection, check out our full comparison of smart contract fuzzing tools.