Halmos is a symbolic execution tool for Ethereum smart contracts developed by a]]16z. Unlike traditional testing that checks specific inputs or fuzzing that explores random inputs, Halmos uses symbolic values to mathematically verify that properties hold for all possible inputs. It integrates seamlessly with Foundry test suites, allowing developers to upgrade existing fuzz tests into formal proofs with minimal changes.

How Halmos Works

Halmos interprets Foundry tests symbolically rather than concretely:

1// Traditional fuzz test - tests random values
2function testFuzz_withdraw(uint256 amount) public {
3    // Tested with random values like 0, 1, 100, type(uint256).max
4    vm.assume(amount <= balance);
5    vault.withdraw(amount);
6    assertEq(vault.balance(), balance - amount);
7}
8
9// Same test with Halmos - proves for ALL values
10// Halmos treats 'amount' as symbolic, exploring all possibilities

When you run halmos, it:

1. Assigns symbolic values to function parameters
2. Executes the test symbolically, tracking constraints
3. Uses SMT solvers to check if any input can violate assertions
4. Reports counterexamples if violations exist, or confirms the property holds

Installation and Usage

1# Install via pip
2pip install halmos
3
4# Run on a Foundry project
5cd your-project
6halmos
7
8# Run specific test
9halmos --function testSymbolic_withdraw
10
11# With loop bounds (handle loops)
12halmos --loop 10

Halmos automatically detects test files and runs functions matching its naming conventions.

Writing Halmos Tests

Halmos tests look like Foundry tests with a few conventions:

1// SPDX-License-Identifier: MIT
2pragma solidity ^0.8.0;
3
4import "forge-std/Test.sol";
5import "../src/Token.sol";
6
7contract TokenSymbolicTest is Test {
8    Token token;
9    
10    function setUp() public {
11        token = new Token();
12        token.mint(address(this), 1000);
13    }
14    
15    // Prefix with 'check_' for symbolic tests
16    function check_transferPreservesTotalSupply(
17        address to,
18        uint256 amount
19    ) public {
20        // Skip invalid cases
21        vm.assume(to != address(0));
22        vm.assume(amount <= token.balanceOf(address(this)));
23        
24        uint256 supplyBefore = token.totalSupply();
25        
26        token.transfer(to, amount);
27        
28        // This assertion is checked for ALL valid inputs
29        assertEq(token.totalSupply(), supplyBefore);
30    }
31}

The check_ prefix tells Halmos to analyze this function symbolically.

Halmos vs Fuzzing vs Unit Tests

Halmos provides the highest confidence level—when it passes, the property is mathematically proven for all inputs within the explored bounds.

Practical Example: Verifying Token Invariants

1contract TokenInvariantTest is Test {
2    Token token;
3    address[] users;
4    
5    function setUp() public {
6        token = new Token();
7        users.push(address(0x1));
8        users.push(address(0x2));
9        users.push(address(0x3));
10        
11        // Initial distribution
12        token.mint(users[0], 500);
13        token.mint(users[1], 300);
14        token.mint(users[2], 200);
15    }
16    
17    // Prove: sum of balances always equals total supply
18    function check_balancesSumToSupply(
19        uint256 fromIdx,
20        uint256 toIdx,
21        uint256 amount
22    ) public {
23        vm.assume(fromIdx < users.length);
24        vm.assume(toIdx < users.length);
25        vm.assume(fromIdx != toIdx);
26        
27        address from = users[fromIdx];
28        address to = users[toIdx];
29        
30        vm.assume(amount <= token.balanceOf(from));
31        
32        vm.prank(from);
33        token.transfer(to, amount);
34        
35        // Calculate sum of all balances
36        uint256 sum = 0;
37        for (uint i = 0; i < users.length; i++) {
38            sum += token.balanceOf(users[i]);
39        }
40        
41        // Prove this holds for ALL valid transfers
42        assertEq(sum, token.totalSupply());
43    }
44}

If Halmos completes without finding counterexamples, you've mathematically proven this invariant holds for any valid transfer.

Handling Loops and Bounds

Symbolic execution faces the path explosion problem with loops. Halmos handles this with bounded analysis:

1# Analyze loops up to 5 iterations
2halmos --loop 5
3
4# Increase for more thorough analysis (slower)
5halmos --loop 20

For loops with known bounds, this provides complete coverage. For unbounded loops, you get guarantees up to the specified bound.

When Halmos Finds a Bug

When a property can be violated, Halmos outputs a counterexample:

1[FAIL] check_withdrawNeverExceedsBalance(uint256)
2Counterexample:
3    amount = 1000000000000000000000000001
4    
5Call trace:
6    withdraw(1000000000000000000000000001)
7    -> balance underflow

This concrete counterexample helps developers understand exactly how the vulnerability can be triggered.

Limitations

Loop bounds: Unbounded loops require setting explicit bounds, providing guarantees only up to that bound.

External calls: Calls to external contracts are difficult to reason about symbolically without modeling those contracts.

Complex math: Some operations (keccak256, ecrecover) are treated as uninterpreted functions, limiting reasoning about their results.

Computation time: Complex contracts with many paths can take significant time to analyze.

Integration with Security Workflows

Halmos fits into a layered security approach:

1. Unit tests: Fast feedback during development
2. Fuzz tests: Broad coverage with random exploration
3. Halmos: Mathematical proofs for critical properties
4. Manual audit: Human review for business logic and design

For high-value contracts, Halmos provides the mathematical certainty that fuzzing approximates but can't guarantee. Major protocols like Uniswap and Aave use symbolic verification for their most critical code paths.

Comparison with Other Formal Verification Tools

Halmos's strength is its low barrier to entry—if you can write Foundry tests, you can write Halmos tests.