What's the difference between SMT solvers and formal verification?

Question

The question holds. What's the difference between the two? What would be an example of using these two tools on a minimal piece of solidity code?

Answer 1

The two terms represent quite different things:

Formal Verification (FV) is a generic term for applying formal methods (FM) to verify the correctness of hardware, software, abstract models, etc. Applying FM means anything based on mathematical proofs, in software often used as a proof of correctness or proof of "bug". The Wikipedia page on FV is actually quite good.

SMT stands for Satisfiability Modulo Theories and extends SAT solvers (which solve the Boolean Satisfiability problem). SMT solvers are concrete tools, automated theorem provers that take in a Boolean formula written in SMT theories (such as Integers, Reals, Arrays, Tuples, etc) and apply specialized decision procedures to answer the question "is this formula ever true?". The solver may answer satisfiable, if there is a valuation of the variables that leads to the entire formula being true, unsatisfiable if it is impossible for the formula to ever be true, or unknown, if the solver was unable to find a decisive answer. The unknown case may happen if you give the solver a timeout, for example, or if you used theories that are complicated to solve, such as Nonlinear Integer Arithmetic (which is undecidable so you can only hope for the best). You can play with the z3 SMT solver in their brand new docs/tutorial page.

Within the FV field, there are several techniques that are used to verify systems (hw, sw, etc). Some of them are graph based, where you define your program and the properties you want to check in terms of a transition system, and you make graph queries of the form "can this bad state ever be reached?", like in Model Checking.

Nowadays, one of the main techniques is a specialization of the above called Symbolic Model Checking, where instead of using an explicit graph you represent the system and properties you want to verify as theorems. That's where SAT and SMT solvers come in. Instead of asking a graph "can my explicit bad state S be reached from my initial state I?", you would represent the same reachability problem as a Boolean formula (potentially using SMT theories), such that an SMT solver will answer unsatisfiable if S cannot be reached from I, and satisfiable otherwise. In summary the former means your property is proven to be correct for every input case ever backed by a mathematical proof, and the latter means there's at least one buggy path in your program leading I to S, where the valuation of the variables is the counterexample to your property.

As a more concrete toy example, take the following Solidity function:

function property(uint16 x, uint16 y) external pure {
    require(x < 100);
    require(y < 100);
    assert(x + y < 1000);
}

Usually FV tools treat constructs like requires as assumptions/pre-conditions. We're not trying to prove the requires, we're assuming they're always true when continuing the execution path. Our target is the assert condition. We want to prove that, given a uint16 x and uint16 y, such that both are < 100, their sum is < 1000. This is of course quite trivial to solve just by looking at it, but it serves as an example of how an SMT solver can be used here. From that code, we'll write the following theorem (basically consisting of a set of constraints):

x >= 0 && x < 2**16      && // type constraints on x
y >= 0 && y < 2**16      && // type constraints on y
x < 100                  && // require(x < 100)
y < 100                  && // require(y < 100)
x + y >= 1000               // negation of our assertion

The reason we negate the assertion we want to prove is that we're looking for a proof by contradiction: if the solver says unsatisfiable to the above, it means it's impossible for the assertion to be false (therefore broken), therefore the assertion must always be true!

Here's the full smtlib2 file to prove the above, you can run it with $ z3 theorem.smt2:

(declare-const x Int)
(declare-const y Int)

(assert (and
    (>= x 0)
    (< x 65536)
    (>= y 0)
    (< y 65536)
    (< x 100)
    (< y 100)
    (not (< (+ x y) 1000))
))

(check-sat)

The solver says unsat. We've now proven our assertion is correct, thus always true regardless of the input values. For the sake of comparison, we can change our property to something less true: assert(x + y < 150). The full theorem in smtlib2:

(declare-const x Int)
(declare-const y Int)

(assert (and
    (>= x 0)
    (< x 65536)
    (>= y 0)
    (< y 65536)
    (< x 100)
    (< y 100)
    (not (< (+ x y) 150))
))

(check-sat)
(get-model)

The solver now says

sat
(
  (define-fun x () Int
    51)
  (define-fun y () Int
    99)
)

The sat answer means our assertion is not always true, and the model that follows gives us exactly how to break the assertion: pass 51 and 99 for x and y in our function. This is a counterexample to our broken property.

The approach above is also called Symbolic Execution and is an example of what many tools do under the hood, for example Solidity's SMTChecker, hevm, Halmos, Manticore.

There are also other more complex techniques that are applied on top of SMT solving a theorem and will give you different pros/cons in tooling, for example Horn solving (used by SMTChecker's CHC engine, solc-verify) and Abstract Interpretation (used by Certora afaik). I try to keep a list of FV tools for Ethereum.