Formal Verification with Halmos: Proving Properties, Not Just Testing Them

There’s a quiet confidence that comes from a green test suite. There’s a quieter dread that comes from knowing it isn’t enough.

Unit tests check the inputs you thought of. Fuzz tests check inputs a machine randomly generates. Both are valuable. Neither can tell you something doesn’t exist — only that they haven’t found it yet. That asymmetry is the fundamental limitation of sampling-based testing: while Foundry, Echidna, or Medusa can verify the presence of a bug relatively fast, they cannot, in general, assert their absence.

Formal verification can. That’s not marketing — it’s the mathematical distinction between finding counterexamples and proving their non-existence. This article covers how Halmos brings that capability into the Foundry workflow, what it takes to use it effectively, and where it genuinely pays off.

---

What Symbolic Execution Actually Is

To understand Halmos, you need to understand what symbolic execution is doing under the hood — because it differs fundamentally from both unit testing and fuzzing.

In a normal unit test, you pass concrete values: transfer(alice, 100). The EVM executes one path through the code. In a fuzz test, you pass randomly generated values and repeat that many times, hoping to hit something interesting. In symbolic execution, you pass a symbol — a mathematical placeholder that represents every possible value simultaneously.

Symbolic execution represents an execution trace as a mathematical formula over symbolic input values — otherwise called a path predicate. An SMT solver is then used to check if a path predicate is “satisfiable” — i.e., whether there exists a value that can satisfy the formula.

The execution engine walks through the EVM bytecode. When it encounters a branch — an if statement, a require, a > comparison — it forks. At every conditional branch, the execution forks into two paths: one where the condition is true and one where it is false. Each path accumulates a set of constraints — the “path condition” — that describes exactly which concrete inputs would follow that path.

When the engine reaches an assertion, a revert condition, or the end of a function, it asks a constraint solver (typically an SMT solver like Z3) whether the accumulated path condition is satisfiable. If the solver finds that a path leading to an assertion violation is satisfiable, it produces a concrete counterexample — specific input values that trigger the bug. This counterexample is immediately usable as a test case, making symbolic execution findings highly actionable.

How It Differs from Fuzzing

The field of symbolic testing is closely related to fuzz testing, with the difference that, instead of trying random inputs in order to break system properties or invariants, Halmos will check an invariant against the whole range of valid inputs.

The practical consequence is significant. A fuzzer might run 100,000 iterations and miss a bug that only appears at amount == type(uint128).max - 1. Symbolic execution doesn’t sample. It represents the entire input space algebraically and asks whether any value in it could violate your property.

Symbolic testing involves executing tests with symbolic values, significantly reducing the need for extensive specifications. Unlike conventional testing, which confirms program functionality for specific inputs, symbolic testing evaluates a program against all conceivable inputs.

The tradeoff is cost. Exploring all paths through a nontrivial function can be computationally expensive, and some path spaces are too large to explore completely. But within those bounds — which you control — the guarantee is exact.

---

Halmos: Symbolic Execution in Your Foundry Test Suite

Halmos is a symbolic testing tool for EVM smart contracts, developed by a16z crypto. It simplifies the process by using existing tests as the basis for formal specifications, instead of requiring new specifications or languages.

That design decision is what makes Halmos accessible. Tools like Certora require you to learn the Certora Verification Language (CVL). K-based tools require K specifications. Halmos is an open-source tool that is smaller in scale and currently lacks some features provided by Certora, but it is meant to serve as a public good and is intended as a niche solution for quickly verifying smart contracts without the need for extensive setup and maintenance.

Halmos is a symbolic testing tool for EVM smart contracts. A Solidity/Foundry frontend is currently offered by default, with plans to provide support for other languages, such as Vyper and Huff, in the future.

The Foundry Relationship

Halmos integrates directly with Foundry — developers write test functions using standard Foundry syntax with symbolic inputs, and Halmos explores all execution paths through those tests. This means teams already using Foundry for testing can adopt symbolic execution with zero new syntax or tooling.

The workflow looks like this:

1. Write a test contract that inherits from both Test (Foundry) and SymTest (Halmos).
2. In your test functions, replace concrete values with symbolic variables created via the svm cheatcode.
3. Assert properties that should hold for all inputs.
4. Run halmos instead of forge test.

Halmos compiles your Foundry project normally, then symbolically executes every function whose name starts with check_ (by convention), exploring all feasible execution paths through the EVM bytecode and checking that no assertion is violated.

Installation

# Install via uv (recommended)
curl -LsSf https://astral.sh/uv/install.sh | sh
uv tool install halmos

# Or via pip
pip install halmos

# Add halmos-cheatcodes to your Foundry project
forge install a16z/halmos-cheatcodes

---

Writing Symbolic Tests

The svm Cheatcode Interface

Halmos cheatcodes are abstract functions designed to facilitate writing symbolic tests, such as the creation of new symbolic values at runtime.

The full SVM interface provides typed symbolic creation:

// Available symbolic constructors
svm.createUint256(string memory name) → uint256
svm.createInt256(string memory name)  → int256
svm.createAddress(string memory name) → address
svm.createBool(string memory name)    → bool
svm.createBytes32(string memory name) → bytes32
svm.createBytes4(string memory name)  → bytes4
svm.createBytes(uint256 size, string memory name) → bytes

It’s important to understand that the created symbol represents a set of all integers within the range of [0, 2^256 - 1], rather than being a random value selected from the range. By using a symbolic value, you can check if the given tests pass for all possible configurations, rather than just a randomly selected setup.

A Minimal Example: ERC-20 Transfer

Here’s how you’d structure a basic symbolic test for an ERC-20 token:

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

contract MyTokenSymbolicTest is SymTest, Test {
    MyToken token;
    address owner;

    function setUp() public {
        owner = address(0xBEEF);
        // Symbolic initial supply: covers all possible uint256 values
        uint256 initialSupply = svm.createUint256("initialSupply");
        vm.prank(owner);
        token = new MyToken(initialSupply);
    }

    /// @notice Proves that a transfer can never increase total supply
    function check_transfer_preserves_total_supply() public {
        address sender   = svm.createAddress("sender");
        address receiver = svm.createAddress("receiver");
        uint256 amount   = svm.createUint256("amount");

        uint256 supplyBefore = token.totalSupply();

        vm.prank(sender);
        // Use try/catch or low-level call so reverts don't abort exploration
        try token.transfer(receiver, amount) {} catch {}

        assertEq(token.totalSupply(), supplyBefore, "Total supply must never change on transfer");
    }

    /// @notice Proves that a transfer can never increase caller's balance
    ///         when called by someone other than the receiver
    function check_transfer_no_self_mint() public {
        address caller   = svm.createAddress("caller");
        address receiver = svm.createAddress("receiver");
        uint256 amount   = svm.createUint256("amount");

        vm.assume(caller != receiver);
        vm.assume(token.balanceOf(caller) > 0);

        uint256 callerBefore = token.balanceOf(caller);

        vm.prank(caller);
        try token.transfer(receiver, amount) {} catch {}

        // Caller's balance must not increase
        assertLe(token.balanceOf(caller), callerBefore, "Sender balance must not increase");
    }
}

Note the naming convention: functions prefixed with check_ are picked up by Halmos. Functions prefixed with test_ are picked up by Foundry. You can have both in the same file, running concrete tests with forge test and symbolic proofs with halmos.

Constraining the Input Space with vm.assume

In symbolic tests, avoid using bound() as it tends to perform poorly. Instead, use vm.assume() which is more efficient and enhances readability:

// ❌ Avoid: bound() adds arithmetic constraints that bloat the solver query
uint256 amount = svm.createUint256("amount");
amount = bound(amount, 1, MAX_AMOUNT);

// ✅ Prefer: vm.assume() expresses a clean precondition
uint256 amount = svm.createUint256("amount");
vm.assume(amount >= 1 && amount <= MAX_AMOUNT);

vm.assume tells the symbolic engine to prune paths that violate the predicate before they propagate further. bound achieves similar semantics but by wrapping the variable arithmetically, which creates additional constraints the solver has to reason through.

Using vm.prank with Symbolic Addresses

The prank() cheatcode can be used to set msg.sender to the symbolic sender address, enabling you to check properties across all possible callers:

function check_only_owner_can_mint() public {
    address caller = svm.createAddress("caller");
    uint256 amount = svm.createUint256("amount");

    // Exclude the owner from this check
    vm.assume(caller != token.owner());

    uint256 supplyBefore = token.totalSupply();

    vm.prank(caller);
    (bool success,) = address(token).call(
        abi.encodeWithSignature("mint(address,uint256)", caller, amount)
    );

    // If the call succeeded, supply must not have changed (non-owner can't mint)
    if (success) {
        assertEq(token.totalSupply(), supplyBefore, "Non-owner must not be able to mint");
    }
}

---

The SMT Solver Relationship

Halmos doesn’t do the math itself — it delegates to a Satisfiability Modulo Theories (SMT) solver. It runs the EVM code of the contract, modeling each instruction as SMT constraints against the inputs, and then Z3 solves for satisfying assignments.

The Z3 SMT solver, developed by Microsoft Research, provides the computational engine for this verification process. SMT solvers extend SAT solvers with theories — arithmetic over integers and bit-vectors, array theories for memory and storage, and more. The EVM maps naturally: storage is an array, arithmetic is bitvector arithmetic over 256-bit words, and control flow is a set of constraints.

When Halmos finishes exploring a path, it hands the accumulated path condition to Z3 as an SMT query: “Is there an assignment of the symbolic variables that makes all these constraints true and violates the assertion?” If Z3 says “unsat” (unsatisfiable) — no such assignment exists — the property holds on that path. If Z3 returns “sat” — it provides a model: concrete values that trigger the violation.

SMT solving excels at full proofs: if Z3 can’t find a model that breaks your invariant, you’ve achieved the cryptographic equivalent of “Q.E.D.”

This solver interaction has performance implications. Some queries are cheap — linear arithmetic over a handful of variables. Others are expensive or undecidable — nonlinear multiplication of two symbolic 256-bit values, for instance. Formal verification tools often use SMT solvers and other constraint solvers in their underlying layer, and these solvers rely on computationally intensive procedures. It is not always possible for program verifiers to determine if a property can be satisfied or not (the “decidability problem”) because a program might never terminate. As such, it may be impossible to prove some properties for a contract even if it’s well-specified.

---

Path Explosion: The Core Scalability Problem

Path explosion is the primary reason symbolic execution doesn’t simply replace all other testing. Using symbolic execution can run into the path explosion problem, where there are too many paths for a computer to explore in a reasonable amount of time and a solver would never be able to finish.

Every branch doubles the path count. A function with 10 independent boolean conditions has up to 1,024 paths. Loops are especially dangerous — an unbounded loop over a symbolic count can produce infinitely many paths. Halmos symbolically iterates unbounded loops only up to a specified bound. For instance, if the bound is set to 3, Halmos will iterate the loop at most 3 times and will not consider input values that would cause the loop to iterate more.

Practical Bounding Strategies

1. Loop bounds with --loop

halmos --loop 3

This caps iteration count globally. For proofs that require more iterations, increase it — but understand the verification only holds for the bounded case.

2. Array size with --array-lengths

Halmos currently requires dynamically-sized arrays, including bytes and string, to be given with a constant size. In the case of test parameters, the size of dynamic arrays can be specified using the --array-lengths option, or it will be set to the default value if not explicitly specified.

halmos --array-lengths data=64

3. Solver timeouts

# Set a 30-second timeout per solver query
halmos --solver-timeout-assertion 30000

Halmos invokes external solvers with unpredictable timings, so these are a source of unpredictability. The number of paths explored may differ between invocations, because the branching solver may have successfully excluded a path (unsat) in one run, but not in the next run (timeout).

4. Decompose tests

Rather than writing one massive symbolic test, decompose into focused property checks. A test that verifies a single invariant over a single function call will terminate quickly. A test that explores 3 chained calls with symbolic selectors may not terminate at all.

5. Concretize unimportant values

Not every variable needs to be symbolic. If you’re proving a transfer property, the name and symbol of the token are irrelevant — deploy with concrete values. Only make symbolic the variables whose full range matters for the property you’re proving.

---

Practical Use Cases

1. Arithmetic Property Verification

Arithmetic is where symbolic execution shines brightest. Symbolic execution precisely determines the input values where integer overflow, underflow, or division by zero occurs.

Consider a vault that computes shares using fixed-point math:

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

contract Vault {
    uint256 public totalAssets;
    uint256 public totalShares;
    uint256 constant PRECISION = 1e18;

    function deposit(uint256 assets) external returns (uint256 shares) {
        if (totalShares == 0) {
            shares = assets;
        } else {
            shares = (assets * totalShares) / totalAssets;
        }
        totalAssets += assets;
        totalShares += shares;
    }

    function withdraw(uint256 shares) external returns (uint256 assets) {
        assets = (shares * totalAssets) / totalShares;
        totalShares -= shares;
        totalAssets -= assets;
    }
}

contract VaultSymbolicTest is SymTest, Test {
    Vault vault;

    function setUp() public {
        vault = new Vault();
    }

    /// @notice Proves that withdraw(deposit(x)) >= x - 1 (rounding loss bounded)
    function check_deposit_withdraw_roundtrip() public {
        uint256 assets = svm.createUint256("assets");
        vm.assume(assets > 0 && assets < type(uint128).max);
        vm.assume(vault.totalAssets() == 0); // clean state

        uint256 shares = vault.deposit(assets);

        vm.assume(shares > 0);
        uint256 recovered = vault.withdraw(shares);

        // Allow at most 1 wei of rounding loss
        assertGe(recovered + 1, assets, "Rounding loss exceeds 1 wei");
    }

    /// @notice Proves totalAssets >= totalShares * rate invariant is maintained
    function check_no_free_shares() public {
        uint256 assets = svm.createUint256("assets");
        vm.assume(assets > 0 && assets < type(uint128).max);
        vm.assume(vault.totalAssets() > 0 && vault.totalShares() > 0);

        uint256 sharesBefore = vault.totalShares();
        uint256 assetsBefore = vault.totalAssets();

        vault.deposit(assets);

        // Shares issued must be proportional — no free shares
        assertGe(
            vault.totalAssets() * sharesBefore,
            vault.totalShares() * assetsBefore,
            "Share issuance broke proportionality"
        );
    }
}

If there’s an overflow path in the multiplication assets * totalShares, Z3 will find the exact values that trigger it and report them as a counterexample.

2. Access Control Proofs

Access control is well-suited to formal verification because the property is crisp: “no address other than X can call function Y.”

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

contract ProtectedRegistry is Ownable {
    mapping(address => bool) public whitelist;
    uint256 public fee;

    constructor() Ownable(msg.sender) {}

    function addToWhitelist(address account) external onlyOwner {
        whitelist[account] = true;
    }

    function setFee(uint256 newFee) external onlyOwner {
        fee = newFee;
    }

    function removeFromWhitelist(address account) external onlyOwner {
        whitelist[account] = false;
    }
}

contract AccessControlSymbolicTest is SymTest, Test {
    ProtectedRegistry registry;
    address owner;

    function setUp() public {
        owner = address(0xBEEF);
        vm.prank(owner);
        registry = new ProtectedRegistry();
    }

    /// @notice Proves that no non-owner can modify the whitelist
    function check_only_owner_can_whitelist() public {
        address caller  = svm.createAddress("caller");
        address target  = svm.createAddress("target");

        vm.assume(caller != owner);

        bool whitelistBefore = registry.whitelist(target);

        vm.prank(caller);
        (bool success,) = address(registry).call(
            abi.encodeWithSignature("addToWhitelist(address)", target)
        );

        // If it succeeded (didn't revert), the whitelist must not have changed
        if (success) {
            assertEq(registry.whitelist(target), whitelistBefore,
                "Non-owner changed whitelist");
        }
    }

    /// @notice Proves that no non-owner can change the fee
    function check_only_owner_can_set_fee() public {
        address caller = svm.createAddress("caller");
        uint256 newFee = svm.createUint256("newFee");

        vm.assume(caller != owner);

        uint256 feeBefore = registry.fee();

        vm.prank(caller);
        (bool success,) = address(registry).call(
            abi.encodeWithSignature("setFee(uint256)", newFee)
        );

        if (success) {
            assertEq(registry.fee(), feeBefore, "Non-owner changed fee");
        }
    }
}

If any path through addToWhitelist is reachable without reverting when caller != owner, Halmos will report it with the exact caller and target values.

3. Invariant Verification

Halmos can help developers bridge the gap between invariant testing and formal verification by allowing them to reuse the same properties written for invariant testing for formal specifications through symbolic testing. Similarly, Halmos can be used for invariant testing to prove that protocol invariants hold up to some arbitrary number of transactions.

A classic invariant for any token: the sum of all balances must equal the total supply. Proving this across arbitrary transfers is a meaningful guarantee:

contract TokenInvariantTest is SymTest, Test {
    MyToken token;
    address[] accounts;

    function setUp() public {
        token = new MyToken(1_000_000e18);

        // Seed symbolic accounts with symbolic balances
        for (uint256 i = 0; i < 3; i++) {
            address acct = svm.createAddress("account");
            uint256 bal  = svm.createUint256("balance");
            // Give each account a symbolic balance via deal
            vm.assume(bal <= token.totalSupply());
            deal(address(token), acct, bal);
            accounts.push(acct);
        }
    }

    /// @notice After any transfer, balances of non-participants are unchanged
    function check_transfer_isolation() public {
        address sender   = svm.createAddress("sender");
        address receiver = svm.createAddress("receiver");
        address observer = svm.createAddress("observer");
        uint256 amount   = svm.createUint256("amount");

        vm.assume(observer != sender && observer != receiver);

        uint256 observerBalanceBefore = token.balanceOf(observer);

        vm.prank(sender);
        try token.transfer(receiver, amount) {} catch {}

        assertEq(
            token.balanceOf(observer),
            observerBalanceBefore,
            "Transfer affected a non-participant's balance"
        );
    }
}

For multi-step stateful invariant testing, the core idea is that within a single stateless test, you can chain together multiple calls, retaining state between them:

/// @notice Prove the DAI-style fundamental equation holds for up to N transactions
function check_fundamental_equation(bytes4[] memory selectors) public {
    vm.assume(selectors.length <= 3); // bound the depth

    for (uint256 i = 0; i < selectors.length; i++) {
        // Make a symbolic but valid call to the protocol
        bytes memory data = calldataFor(selectors[i]);
        (bool success,) = address(protocol).call(data);
        vm.assume(success); // only consider non-reverting paths
    }

    // Assert the invariant holds after any sequence of valid calls
    assertEq(
        protocol.totalDebt(),
        protocol.totalCollateral() - protocol.reserveFactor(),
        "Fundamental equation violated"
    );
}

---

What Formal Verification Can and Cannot Prove

Understanding the scope of what Halmos can prove is as important as understanding how to use it.

What It Can Prove

Arithmetic properties. Symbolic execution precisely determines the input values where integer overflow, underflow, or division by zero occurs. This makes it ideal for verifying safe math properties, bounding rounding error, and proving conservation laws in DeFi math.

Access control. That only the owner can call privileged functions, that role-based guards work correctly for all possible callers, and that privilege escalation paths don’t exist.

Conservation invariants. That tokens are neither created nor destroyed during transfers, that vault solvency ratios are maintained, that the total balance across accounts equals total supply.

Reachability properties. That a particular state (e.g., paused == true && totalSupply > 0) is either always reachable or never reachable under the defined preconditions.

Absence of specific bugs. If you write a property that characterizes a bug class (e.g., “no transfer can increase the sender’s balance”), Halmos can prove that bug class doesn’t exist in your implementation.

What It Cannot Prove

Specification correctness. Halmos proves that your code satisfies your properties — not that your properties correctly capture your intent. A wrong specification produces a meaningless proof.

Economic security. Oracle failures — if the price feed is manipulated, the contract will execute “correctly” with bad data. Flash loan attacks, MEV exploits, and governance manipulation are economic phenomena that formal verification of individual contract logic cannot prevent.

Cross-contract reentrancy (without mocks). Halmos analyzes contracts in isolation. Multi-contract reentrancy involving untrusted external contracts requires you to model the adversarial external contract explicitly, which may be out of scope for automated verification.

Unbounded properties. If a property requires proving something holds over an unbounded number of transactions, and you can’t express it within a bounded loop, Halmos cannot prove it. The bounded nature of its exploration means results are always conditional: “this property holds for all inputs, given at most N loop iterations.”

Non-deterministic behavior. Block hash, timestamp, and other environmental values that are truly non-deterministic at the EVM level require careful treatment. Halmos does model these symbolically, but complex dependencies on them can exhaust solver resources.

---

Halmos vs. Other Formal Verification Tools

When comparing Halmos with other formal tools that support EVM bytecode: K is a powerful formal verification framework that enables deductive verification and interactive theorem proving. Its underlying theory and implementation provide a high level of expressiveness, making it suitable for verifying complex programs and algorithms. However, K is not designed with heavy emphasis on automated verification and lacks certain automation features, which can require more manual effort during the verification process.

Both HEVM and Halmos have the feature of not requiring a separate specification and can symbolically execute existing tests to identify assertion violations. This allows users to use both tools interchangeably or run them in parallel for the same tests, providing them with multiple options for symbolic testing. It’s worth noting that, despite their similarities, HEVM and Halmos have been independently developed and differ in their implementation details — particularly in terms of optimizations and symbolic reasoning strategies.

The design space roughly looks like this:

Tool	Spec Language	Automation	Expressiveness	EVM Model
Halmos	Solidity/Foundry	High	Moderate	Approximate
HEVM	Solidity/dapptools	High	Moderate	Approximate
Certora Prover	CVL	Moderate	High	Complete
Kontrol (K)	K specification	Low	Highest	Formal
Mythril	None (automated)	Very High	Low	Approximate

While Halmos is a valuable addition to the toolset available for smart contract verification, it is meant to complement (not replace) existing tools. Developers can combine Halmos with other tools to achieve a higher level of assurance in their contracts.

---

When Formal Verification Is Worth the Investment

Formal verification has real costs: engineering time to write properties, solver time to check them, and cognitive overhead to interpret results. It isn’t always the right choice. Here’s a framework for deciding when it is.

Strong Candidates

High-value, low-complexity contracts. A token contract holding $100M in assets is a perfect target. The codebase is small, the properties are clear (conservation, access control), and the cost of a bug is enormous.

Reusable primitives. Libraries, base contracts, and core protocol math that hundreds of contracts will depend on. The verification effort amortizes across all consumers.

Upgrade-sensitive logic. When you’re upgrading a contract that holds significant assets, formal verification of the delta — proving the new implementation satisfies the same invariants as the old — provides strong assurance that the upgrade is safe.

Regulatory or audit requirements. Some institutional deployment contexts require machine-checked proofs. Halmos’s output can be part of an audit artifact.

Weaker Candidates

Rapidly iterating codebases. If the contract changes every sprint, maintaining symbolic tests at pace with development adds friction without proportionate benefit.

Complex multi-contract systems without good mocking. The mental model of symbolic testing is to ensure that a given contract behaves as expected against all possible inputs and external contracts’ states. To achieve this, external contracts need to be mocked to represent their arbitrary storage states. Systems with many external dependencies that are hard to mock accurately may produce vacuous proofs.

Properties that are inherently economic. If the risk model is primarily MEV, governance attacks, or oracle manipulation, symbolic execution of isolated contract logic won’t capture it.

The Practical Starting Point

In practice, prove non-negotiables such as access control, value conservation, caps and bounds, and pause or oracle safety with a verifier, and rely on tests and fuzzing for integration and performance. Together they provide defense in depth: tests show the code works for the cases you tried, formal methods show it cannot break in the cases you did not.

Start with the properties you’re most confident about. Access control in an Ownable contract is easy to specify and fast to verify. Get one green halmos run, understand what it proved and what it didn’t, then expand scope incrementally.

---

Putting It All Together: A Verification Checklist

Before running Halmos on a new contract, work through this checklist:

1. Identify your critical properties. Conservation laws, access guards, bounded outputs. Write them down in English before writing them in Solidity.

2. Scope the symbolic variables. Every svm.create* call expands the input space. Only make symbolic what matters for the property.

3. Use vm.assume for preconditions. Express the domain of validity before the call under test. Don’t prove properties over impossible states.

4. Handle reverts intentionally. Halmos ignores reverting paths by default.

When a function reverts under symbolic execution, Halmos treats that path as infeasible by default — it does not check whether the revert itself was correct. To assert that a function should revert under specific conditions, use vm.expectRevert before the call, or check success via a low-level call pattern.

// Assert that withdraw reverts when the caller has no balance
function check_withdrawRevertsOnZeroBalance(address caller) public {
    vm.assume(vault.balanceOf(caller) == 0);
    vm.prank(caller);
    (bool success,) = address(vault).call(
        abi.encodeCall(vault.withdraw, (1))
    );
    assert(!success); // Must revert
}

---

Halmos Audit Checklist

Setup

• Halmos version is pinned and matches the Foundry environment
• halmos.toml or CLI flags set --loop to cover all relevant loop bounds
• --solver-timeout is configured to avoid silent timeouts masking unproven properties

Symbolic variable scope

• Only variables that matter for the property under test are made symbolic
• Address variables are constrained with vm.assume to exclude known-invalid states (e.g., address(0))
• Amount variables are bounded to realistic ranges to reduce solver search space

Property design

• Every assert is preceded by meaningful preconditions via vm.assume
• Properties are not trivially true (e.g., assert(true)) — all assertions have been reviewed for vacuity
• Revert cases are explicitly tested with low-level calls and assert(!success) patterns

Counterexample triage

• Every counterexample produced by Halmos has been investigated — not suppressed with vm.assume
• Counterexamples that represent real bugs are tracked and fixed before deployment
• Counterexamples that represent spec bugs have been documented with justification

Integration

• Halmos runs in CI on every PR that modifies core arithmetic or state-transition logic
• Properties are versioned alongside the contract — a property written for V1 is updated when V2 changes the invariant