Formal Verification for Solidity: Halmos and Certora

# Formal Verification for Solidity: Halmos and Certora

Most Solidity testing answers the question "does this work for the cases I tried?" Fuzzing widens that to "does this work for thousands of random cases?" Formal verification asks a stronger question: "is there any input, anywhere, that breaks my property?" When the answer is no, you get a mathematical proof rather than a green checkmark. This article explains what verification adds on top of fuzzing, how to write properties and invariants, and how two practical tools, Halmos and the Certora Prover, approach the job.

What formal verification adds beyond fuzzing

A fuzzer like Foundry's built-in engine samples concrete inputs. It is fast, cheap, and catches a lot of bugs, but it can only ever explore a finite slice of the input space. If a vulnerability lives in one specific value of a uint256, the fuzzer may never roll those dice.

Formal verification tools reason about all inputs at once. They do this through symbolic execution: instead of running your function with the number 42, they run it with a symbolic variable x that stands for every possible value. The tool then hands the resulting logical constraints to an SMT solver (typically Z3 or a similar backend) and asks: can any assignment of x violate the assertion?

• If the solver says unsat (no such assignment exists), the property holds for every input.

• If it says sat, it returns a concrete counterexample, a specific input that breaks the property.

That counterexample is the practical payoff. You do not just learn that something is wrong; you get the exact transaction that proves it.

The trade-off is path explosion. Loops and deep call stacks multiply the number of paths the solver must consider, so most tools are *bounded*: they verify up to N loop iterations or a fixed call depth. Be honest about that boundary when you read the results.

Properties and invariants

Verification is only as good as the property you write. Two shapes dominate.

Properties (sometimes called rules) describe what a single function call should guarantee. Example: "after transfer(to, amount) succeeds, the sender balance decreases by exactly amount."

Invariants describe a fact that must hold in every reachable state, before and after any function the contract exposes. Example: "the sum of all balances always equals totalSupply." An invariant is the more powerful statement because it constrains the contract across its entire lifecycle, not just one call.

Good properties tend to be:

Total, covering the success and the revert path.

Relational, comparing state before and after rather than asserting a magic constant.

Minimal, so a failure points at one cause.

Halmos: open source, Foundry style

Halmos, from a16z, runs your Foundry-style Solidity tests symbolically. If you already write Foundry tests, the learning curve is small. The convention is a function prefixed with check_ instead of test. Every parameter of that function becomes a symbolic value, so a single check_ function stands in for an entire fuzz campaign, but with a proof at the end.

Here is a property for a minimal token, proving that transfer moves exactly amount and never inflates supply:

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

import {Test} from "forge-std/Test.sol";
import {Token} from "../src/Token.sol";

contract TokenSymbolicTest is Test {
    Token internal token;

    function setUp() public {
        token = new Token();
    }

    // Every parameter here is symbolic: Halmos explores all values.
    function check_transfer(address from, address to, uint256 amount) public {
        vm.assume(from != to);
        vm.prank(from);
        token.mint(from, amount);

        uint256 supplyBefore = token.totalSupply();
        uint256 fromBefore = token.balanceOf(from);
        uint256 toBefore = token.balanceOf(to);

        vm.prank(from);
        bool ok = token.transfer(to, amount);

        if (ok) {
            assertEq(token.balanceOf(from), fromBefore - amount);
            assertEq(token.balanceOf(to), toBefore + amount);
            assertEq(token.totalSupply(), supplyBefore); // supply is conserved
        }
    }
}

You run it from the command line:

halmos --function check_transfer

If the property holds, Halmos reports the path as passing. If it does not, it prints a counterexample with concrete values for from, to, and amount. Because loops are bounded, you control depth explicitly:

halmos --function check_transfer --loop 4

The headline benefit of Halmos is reuse. You leverage the test harness, cheatcodes (vm.assume, vm.prank), and mental model you already have, and you upgrade a fuzz test into a bounded proof by renaming the prefix and tightening the assumptions.

Certora Prover: dedicated specs in CVL

The Certora Prover separates the specification from the test harness. You write properties in a dedicated language, CVL (Certora Verification Language), stored in a .spec file alongside the contract. CVL is built for verification, so it expresses invariants and relational rules directly, and the Prover does not impose the same loop bounds as a Foundry-style runner for many patterns (loops are still handled, often via unrolling that you configure).

A CVL rule mirrors the property above:

rule transferPreservesSupply(address to, uint256 amount) {
    env e;
    require e.msg.sender != to;

    uint256 supplyBefore = totalSupply();
    uint256 senderBefore = balanceOf(e.msg.sender);
    uint256 toBefore      = balanceOf(to);

    transfer(e, to, amount);

    assert totalSupply() == supplyBefore, "supply must be conserved";
    assert balanceOf(e.msg.sender) == senderBefore - amount;
    assert balanceOf(to) == toBefore + amount;
}

Where Certora shines is invariants. The Prover checks an invariant in two steps: it confirms the constructor establishes it, then confirms that every public method preserves it. You do not enumerate the methods; the Prover does. This worked example states that total supply equals the sum of two tracked balances and holds across the whole contract:

invariant supplyEqualsBalances()
    totalSupply() == balanceOf(alice) + balanceOf(bob)
    {
        preserved {
            require alice != bob;
        }
    }

The preserved block lets you state assumptions that must hold before each method runs. You can also restrict which functions an invariant is checked against with a filtered clause, for example skipping a privileged mint that legitimately changes supply.

Choosing between them

| | Halmos | Certora Prover |

|---|---|---|

| Spec language | Solidity (check_ tests) | CVL .spec files |

| Setup | Reuses Foundry harness | Separate spec, config file |

| Cost | Open source, free | Commercial, with community access tiers |

| Sweet spot | Quick bounded proofs, fast iteration | Deep invariants across all methods |

The two are complementary rather than rival. A common workflow is to prototype properties in Halmos because the loop from idea to result is tight, then promote the most important invariants into CVL for the stronger, method-spanning guarantees the Certora Prover provides.

A few cautions hold for either tool. Verification proves the property you wrote, not the property you meant, so a weak spec gives false confidence. External calls and unbounded loops remain hard, and you will often have to model or summarize them. Treat the work as iterative: write a property, get a counterexample, refine, repeat.

Practice it on Solingo

The fastest way to internalize this is to break a property on purpose and watch the counterexample appear. On app.solingo-blockchain.xyz you can write a small token, state an invariant such as supply conservation, introduce a subtle bug, and see how a proof obligation fails where a fuzzer might have stayed green. Start with one invariant, prove it, then try to break it.