Formal Verification of Smart Contracts: A Guide

Formal verification is the highest tier of assurance for testing smart contracts against their intended behavior.

Unit tests and even fuzzing check the inputs that get tried. Formal verification proves that the invariants you specify hold under every possible circumstance, beyond a shadow of a doubt.

This guide explains how formal verification of smart contracts works under the hood, then shows how to start today with the SMTChecker built into Solidity.

Boolean Formulas and Satisfiability

Formal verification works on Boolean formulas. Your contract code is translated into conditions on specific variables, all ANDed and ORed together.

The result is something an SMT solver can interpret. The solver then checks whether the formula is satisfiable.

Satisfiable means some combination of input variables exists that makes the whole formula return true.

Take a function of three variables.

f(x, y, z) = (x > y) AND (y > z) AND (x > z)

Can you find values of x, y and z that make it true? There are many. One is x = 2, y = 1, z = 0.

Two is greater than one, one is greater than zero, and two is greater than zero. True and true and true, so the formula is satisfiable.

A single combination of inputs is all it takes.

From Formula to Contract

Here is the same formula laid out in a smart contract.

contract Formula {
    function check(uint256 x, uint256 y, uint256 z) public pure {
        assert(x > y);
        assert(y > z);
        assert(x > z);
    }
}

Each assert adds one condition to the formula. Several asserts in a row are equivalent to ANDing those conditions together.

To formally verify the contract, every one of these assertions must be verified.

Three ways to verify it

• K and KEVM. Write a full specification of what you want to prove in K, a language designed for this kind of proving, then use the KEVM repository to prove it for a contract.
• SMT-LIB and Z3. Translate the contract into SMT-LIB, the language SMT solvers take as input, and feed it to the Z3 prover.
• The SMTChecker. The easiest option is built into Solidity itself. Under the hood, it converts your contract into SMT-LIB and feeds it to Z3 for you.

Running the SMTChecker

You run the SMTChecker through solc. Depending on your setup and platform, you may have to build solc yourself to get the SMTChecker working; the Solidity docs have instructions.

The command takes three settings: a model checker engine used during the proof, the solver (Z3 here), and the targets to check.

solc --model-checker-engine all \
     --model-checker-solvers z3 \
     --model-checker-targets assert \
     Formula.sol

The assert target validates the assertions you placed. Other targets come later.

Why the proof fails

The formula is satisfiable, so you might expect the contract to verify. It does not.

The SMTChecker disproves all three assertions with a single counterexample: x = 0, y = 0, z = 0. Look at the asserts again and that is obvious, because they fail for a lot of values.

The reason is that the SMTChecker does not ask whether your formula can be true. It checks for the unsatisfiability of the formula's negation.

Negating f flips each comparison and turns every AND into an OR.

NOT f = (x <= y) OR (y <= z) OR (x <= z)

If the negation can be satisfied, f cannot hold for all inputs. Since the conditions are ORed, one true condition is enough: with x = 0 and y = 0, x <= y already holds.

So the negation is satisfiable, and f is not formally verifiable.

The logic runs the other way too. If the negation of a formula can never be satisfied, the original must hold for every input.

Making the Invariant Hold

To make the assertions pass, limit the scope of the inputs with require statements.

Try it before reading on: which two requires would let all three assertions hold?

One answer is to require y < x and z < y.

contract Formula {
    function check(uint256 x, uint256 y, uint256 z) public pure {
        require(y < x);
        require(z < y);
        assert(x > y);
        assert(y > z);
        assert(x > z);
    }
}

Run the SMTChecker again and all three verification conditions are proved safe.

You have formally verified that the assertions hold for literally every possible x, y and z that satisfies the two requires.

A second example

Now take a contract with two functions. Function h checks that doubling x cannot overflow a uint256, then returns 2 * x.

Function f returns x + 5, which could overflow if x is within five of the maximum uint256. The invariant to verify is that h(x) is always greater than or equal to f(x).

Before running anything, ask yourself whether this verifies as written, and if not, what you would add.

It does not verify as written. The counterexample is x = 0: h(0) is 0, f(0) is 5, and 0 is not greater than or equal to 5.

Add one require, that x is greater than 4, and the SMTChecker proves the invariant safe.

contract Compare {
    function h(uint256 x) public pure returns (uint256) {
        require(x <= type(uint256).max / 2);
        return 2 * x;
    }

    function f(uint256 x) public pure returns (uint256) {
        return x + 5;
    }

    function check(uint256 x) public pure {
        require(x > 4);
        assert(h(x) >= f(x));
    }
}

This gets more powerful as systems get more complex. Math-heavy functions that do many computations are hard to prove out mentally.

The SMTChecker can prove beyond a shadow of a doubt that invariants like this hold in the code. That makes it a key tool for chasing out bugs that are very hard to uncover through manual analysis.

Other Targets

The SMTChecker checks more than assertions. Set the target to overflow on the second contract and it flags f, which is not protected against overflow.

The counterexample is a number only four less than the maximum uint256. Adding 5 to it wraps around to zero, or, in Solidity 0.8 and later, reverts.

Is this unchecked block safe?

Now picture something like a vault. You want to wrap the balance subtraction in an unchecked block to save a little gas.

Is that safe, or is there something else to worry about? Set the targets to all and run the checker.

contract Vault {
    mapping(address => uint256) public balances;

    function deposit(uint256 amount) external {
        balances[msg.sender] += amount;
    }

    function withdraw(uint256 amount) external {
        require(balances[msg.sender] >= amount);
        unchecked {
            balances[msg.sender] -= amount;
        }
    }
}

It reports one potential overflow, on balances[msg.sender] += amount. With any reasonable token, that is extremely unlikely.

It flags nothing on the subtraction. So you have formally verified that this use of unchecked is safe.

The full target list

Run solc --help to see every target. Among them:

• Underflow
• Overflow
• Division by zero
• Balance (insufficient balance for a transfer)
• Assertions
• Popping an empty array
• Out-of-bounds access

These are edge cases you want to know about exactly when they can occur, because they could be used to build a critical vulnerability.

They are also a great way to collect knobs for more complex attacks. A very rare division-by-zero case in a complex system, for instance, could be leveraged as one step of a larger exploit.

Know the Limits

The SMTChecker has limits. Some code is too computationally hard for it to prove.

In those cases, you may need to modify the assert statements, or add and modify require statements, to limit the computation the proof needs.

The best way to learn is to get your hands dirty. Start formally verifying your own contracts with the SMTChecker; it pairs well with mutation testing and the rest of a secure development process.

For where these tools fit in a full review, see how to audit a smart contract.

How Guardian Helps

Every Guardian smart contract audit includes an invariant suite built around solvency, accounting, rounding and edge states, so fixes and future changes can be pressure-tested again and again.

Senior researchers then attack what the invariants leave standing, with exploit-driven review.

Frequently Asked Questions

How is formal verification different from fuzzing?

Unit tests and fuzzing check the inputs that get tried. Formal verification proves that the invariants you specify hold for every possible input, within the constraints your require statements set.

What is the Solidity SMTChecker?

It is a formal verification tool built into the Solidity compiler. It converts your contract into SMT-LIB, passes it to a solver such as Z3, and reports each property as proved safe or gives a counterexample.

Why does the SMTChecker reject an assertion?

It checks whether the negation of your formula is satisfiable. If any input makes an assertion false, it reports that input as a counterexample. Constrain the inputs with require statements, or fix the code.

What can the SMTChecker check besides assertions?

Its targets include overflow, underflow, division by zero, insufficient balance, popping an empty array and out-of-bounds access. Run solc --help to see the full list.

Sources

• Owen Thurm (YouTube): Guide To Formal Verification | Take Security To The Next Level (June 2023)
• Solidity documentation: SMTChecker and Formal Verification