Automated Verification and SMT

Hand-proving a Hoare triple is illuminating once and tedious forever. The dream is to hand a program — annotated with its specification — to a tool, and get back either a green tick ("proved correct for all inputs") or a concrete counterexample. That dream is real, and it runs on two engines bolted together: a verification-condition generator that turns "is this program correct?" into a pile of pure logic formulas, and an SMT solver that decides whether those formulas are true.

The bridge between them is the weakest-precondition calculus. Where Hoare logic gives rules a human stacks by hand, wp makes those rules a mechanical function: feed it the code and the postcondition, and it computes exactly the logical obligations that must hold. Those obligations are the verification conditions, and discharging them is a job for a machine.

From code + annotations to verification conditions

Recall the weakest precondition \mathrm{wp}(C, Q): the least restrictive assertion on the pre-state that guarantees Q after running C. Its defining equations are the engine of VC generation:

Assignment: \mathrm{wp}(x := E,\ Q) = Q[x := E] — substitute E for x in Q.
Sequence: \mathrm{wp}(C_1; C_2,\ Q) = \mathrm{wp}(C_1,\ \mathrm{wp}(C_2, Q)) — push the postcondition backwards through the program.
Conditional: \mathrm{wp}(\texttt{if } b\ C_1\ C_2,\ Q) = (b \Rightarrow \mathrm{wp}(C_1,Q)) \wedge (\neg b \Rightarrow \mathrm{wp}(C_2,Q)).
Loop (needs a supplied invariant I): the loop is cut at I, generating three VCs — establishment, preservation, and usefulness (below).

To verify a routine \{P\}\,C\,\{Q\}, the tool computes \mathrm{wp}(C, Q) and emits the single verification condition P \Rightarrow \mathrm{wp}(C, Q). If that formula is valid (true in every interpretation), the program meets its spec. Loops break the program into finite straight-line chunks at each invariant, so even a program with unbounded loops produces a finite set of loop-free VCs.

A worked VC

Take a routine that computes an absolute value, annotated with its contract and — because there is a branch, not a loop — needing no invariant:

// requires: true // ensures: result >= 0 && (result === x || result === -x) function abs(x: number): number { let result: number; if (x >= 0) { result = x; } else { result = -x; } return result; // Q(result): result >= 0 && (result === x || result === -x) }

Applying wp to the conditional against the postcondition Q \equiv r \ge 0 \wedge (r = x \vee r = -x) gives one VC:

\underbrace{\texttt{true}}_{P} \Rightarrow \big(\, x \ge 0 \Rightarrow Q[r := x] \,\big) \wedge \big(\, x < 0 \Rightarrow Q[r := -x] \,\big)

which after substitution is (x \ge 0 \Rightarrow x \ge 0 \wedge (x = x \vee \dots)) \wedge (x < 0 \Rightarrow -x \ge 0 \wedge (\dots \vee -x = -x)). Each conjunct is a fact of linear arithmetic over the reals: from x < 0 we get -x > 0 \ge 0, and so on. A solver checks it in microseconds. For a loop program you would additionally discharge the three loop VCs — establishment P \Rightarrow I, preservation I \wedge b \Rightarrow \mathrm{wp}(\text{body}, I), and usefulness I \wedge \neg b \Rightarrow Q.

Discharging VCs: SAT versus SMT

A verification condition is a logic formula; deciding validity is the same as deciding whether its negation is unsatisfiable. The workhorse for satisfiability is the SAT solver — decide whether a purely Boolean formula can be made true — the canonical NP-complete problem, yet astonishingly fast in practice on real instances.

But VCs are not purely Boolean. They talk about integers, reals, arrays and functions: x + 2y \le 7, a[i] = a[j], f(u) = f(v). SMT — Satisfiability Modulo Theories — is SAT extended with background theories that give meaning to these symbols. The solver's Boolean engine handles the propositional skeleton and hands atoms like x + 2y \le 7 to a specialised theory solver that knows arithmetic.

Linear arithmetic over integers (LIA) or reals (LRA) — inequalities and sums; the bread and butter of program verification.
Arrays — the \text{read}/\text{write} axioms (\text{read}(\text{write}(a,i,v),i) = v) model the heap and memory.
Bit-vectors — fixed-width machine integers with exact overflow and bitwise operations, for reasoning about real hardware and low-level code.
Uninterpreted functions (EUF) — functions known only to be consistent (u = v \Rightarrow f(u) = f(v)); they abstract away code you don't want to unfold.

Z3 (Microsoft Research) is the best-known SMT solver; CVC5 and Yices are peers. Combining theories (the Nelson–Oppen framework) lets a single query mix arithmetic, arrays and functions at once — which is exactly what a VC over real code needs.

Two answers. First, worst case is not typical case: modern SAT/SMT solvers (CDCL — conflict-driven clause learning) exploit the structure of real formulas so effectively that instances with millions of variables routinely fall in seconds, even though a crafted adversarial instance could stall them. Verification conditions are highly structured, not random. Second, expressiveness is traded against decidability: pure linear integer arithmetic is decidable; add multiplication of variables and you reach the undecidable, so tools restrict what you may write, or return "unknown". A solver's honest possible answers are sat (here's a counterexample), unsat (proved), and unknown — the price of touching an undecidable fragment.

The tool landscape

You rarely write VCs by hand; a verification tool sits between your annotated source and the solver:

Tool	Role
Boogie	An intermediate verification language: front-ends compile to it, it generates VCs and calls Z3. The plumbing many others reuse.
Dafny	A verification-aware programming language (compiles to Boogie→Z3). You write code with `requires`/`ensures`/`invariant`/`decreases` and it proves them as you type.
Why3	A platform with its own language (WhyML) that dispatches VCs to many back-end provers (SMT solvers and interactive ones).
Frama-C	Analyses real C annotated in ACSL; its WP plug-in generates weakest-precondition VCs for industrial C code.

The consistent theme: annotate, generate VCs by wp, discharge with SMT. What the human still owes the tool is the creative part — the loop invariants and termination measures — because those cannot in general be inferred.

Automated verification is not magic correctness. Two gaps bite constantly. First, the loop invariant is your job: the tool needs it to cut each loop into loop-free VCs, and if you supply a weak or wrong invariant the proof simply fails (or, if it is too weak to imply the postcondition, gets stuck) — the solver won't invent the right one for you. Second, and more dangerous, the specification itself is trusted, not checked. If your ensures clause is wrong, incomplete, or vacuously satisfiable, a proof against it certifies nothing useful — the code is proved to meet a spec that doesn't say what you meant. "Verified" always means "verified against these annotations", never "verified to do the right thing". Garbage spec in, green tick out.