Formal verification

Establishing specified properties of a system using formal proofs about a precise model. Formal verification connects an implementation to a formal specification; correctness of the model and its assumptions still matters when applying the result to a physical system.

For a small example, the summation loop verification below starts with executable steps and asks two separate questions: does any returned value satisfy the postcondition, and does execution reach that return? A loop invariant answers the first; a loop variant answers the second. This turns an unbounded family of permitted inputs into a few reusable proof obligations.

The model must specify programming language semantics, including the meaning of variable assignments, comparisons and integer arithmetic. A proof about exact mathematical integers need not describe a machine that wraps on integer overflow. Similarly, a correct formal proof of a weak or mistaken formal specification does not establish the intended behavior. Choosing the right formal specification and relating the model to the implemented system remain substantive tasks.

Software testing examines chosen executions and can expose a counterexample. A formal proof instead justifies a statement throughout its stated model; it does not require executing every permitted input. This makes formal verification valuable when rare boundary cases matter, while software testing can still reveal an incorrect model or misunderstood requirement.

In 1969, Tony Hoare presented rules for variable assignment, composition and iteration in a small programming language. His paper explicitly says those rules do not prove successful termination, and discusses the dependence of arithmetic reasoning on the chosen overflow behavior. These reservations already make the model's scope part of the argument.^[ref]

A condition selecting admissible infinite paths in a transition system, often to exclude executions that postpone an enabled activity forever. The notation $TS{\models }_{\mathrm{fair}}\phi$ quantifies only over initial paths in a transition system satisfying the chosen condition. For example, $GFp$ requires $p$ infinitely often, while $FGp$ requires $p$ permanently from some point onwards. Neither condition implies the other.

A model consisting of a set $S$ of states, a transition relation $\to \subseteq S\times S$, initial states $I\subseteq S$, a set $AP$ of atomic propositions, and a label function $L:S\to 2^{AP}$ identifying which atomic propositions hold at each state. A path in a transition system follows permitted transitions. Some definitions omit labels or initial conditions; specify the convention used in each application.

A transition system whose edges carry action labels. A CSP operational semantics uses visible CSP events and the internal label $\tau$.

A state with no successor in the transition relation. Assuming no terminal states makes every finite path in a transition system extendible and avoids choosing a separate convention for interpreting infinite-path temporal logic at a dead end.

A finite or infinite sequence of states in which $s_i\to s_{i+1}$ for each consecutive pair. In infinite-path linear temporal logic semantics, paths are infinite; an initial path must also start in the specified initial set. Repeated states are allowed, unlike conventions for a simple path in a graph.

An infinite path in a transition system represented by a finite prefix followed by infinite repetition of a nonempty finite loop. If stored positions are $q_0,\dots ,q_k$ and $q_k\to q_{\ell }$, the represented sequence is $q_0\cdots q_{\ell -1}(q_{\ell }\cdots q_k{)}^{\omega }$. The linear temporal logic condition $GFp$ holds exactly when $p$ occurs on the repeated part, and $FGp$ holds exactly when $p$ holds everywhere on that part.

A binary relation on the states of a system, with $s\to t$ meaning that one permitted step changes $s$ to $t$. A Boolean formula can encode a transition relation after choosing bits for the current and next states.

For a state formula $\phi$ in a fixed labelled transition system, its satisfaction set is $\{s\in S:s\models \phi \}$. This is a set of states; it is distinct from the assertion that every initial state satisfies the formula.

A formal verification method that encodes a bounded execution and a violated specification as a Boolean satisfiability problem. A satisfying assignment yields a counterexample. For infinite-path properties, a lasso path can finitely represent a repeated execution. Failure to find a counterexample at one finite bound alone does not prove an unbounded property.^[ref]

Compute $1+2+\cdots +n$, the triangular number $T_n$, for a nonnegative integer $n$. The empty sum gives zero when $n=0$. Use exact mathematical integers and keep the input $n$ unchanged; every comparison and variable assignment is a terminating operation. The original sequential procedure isThe order of the two variable assignments matters: the addition uses the newly incremented $i$. For $n=4$, the pairs $(i,s)$ at successive condition checks are $(0,0),(1,1),(2,3),(3,6),(4,10)$. At the last check, $i<n$ is false, and the returned sum is $10$.

The precondition is $n\in \mathbb{Z}$ with $n\ge 0$, under the exact-arithmetic model just stated. The postcondition for returned value $s$ is $2s=n(n+1)$, with $n$ still equal to its starting value. At each condition check use the loop invariantand the loop variant $V=n-i$. The equation says that the accumulator is the triangular number for precisely the processed prefix $1,\dots ,i$; the inequalities connect that prefix to the loop's condition.

Initialization gives $i=s=0$, so $I$ holds, including when $n=0$. For preservation, let the old values satisfy $I$ and $i<n$. Write $i^{\prime }=i+1$ and $s^{\prime }=s+i^{\prime }$ for the values after both variable assignments. Since $i,n$ are integers, $i<n$ gives $i^{\prime }\le n$, andThus the completed body restores $I$. Between the two variable assignments, the equation can be false; the loop invariant is required at the loop head. This preservation step is mathematical induction on the number of completed iterations.

At exit, the false condition gives $i\ge n$, while $I$ gives $i\le n$. Hence $i=n$, so $2s=n(n+1)$: this proves partial correctness. For algorithm termination, $I$ gives the nonnegative integer $V=n-i$. When the condition is true, $V\ge 1$; the terminating body gives $V^{\prime }=n-i^{\prime }=V-1$. Therefore the loop cannot repeat forever. Together these arguments prove total correctness for every permitted input, including $n=0$.

Two changes expose what the proof checks. Swapping the two body instructions computes $0+1+\cdots +(n-1)$, returning $6$ rather than $10$ for $n=4$. Leaving $i$ unchanged can preserve an initial equation forever without producing any answer. The first change breaks the intended postcondition; the second breaks algorithm termination. A trace can reveal these failures, while the two proof obligations explain them.

The exact-arithmetic assumption has a concrete boundary. In a stipulated unsigned eight-bit model where each addition wraps modulo $256$, $n=23$ fits in the input representation, but its intended triangular number is $276$. The stored accumulator instead finishes at $20$, so the mathematical postcondition fails. This is integer overflow, and the proof above does not apply to that altered model. Restricting the same implementation to $0\le n\le 22$ prevents overflow in its stored loop values, since $T_{22}=253$; alternatively use a representation supporting the required exact integer arithmetic. The equations in the proof are mathematical statements, not instructions to evaluate products in eight bits.

A mathematically precise description of permitted behaviour. A formal specification for the microkernel file-read example's service could relate an authorized request to the exact returned bytes; a formal specification of its microkernel's IPC need only describe the protected transport operation. They state different obligations.

For the summation loop verification, require a nonnegative integer input $n$ and a returned value $s$ satisfying $2s=n(n+1)$. The formal specification describes what answer is acceptable without requiring this particular loop: another implementation may satisfy the same contract. State separately whether partial correctness or total correctness is required. A Hoare triple packages the precondition, the program and the postcondition; Hoare logic supplies rules for establishing such claims.

Precision alone does not ensure a useful requirement. The postcondition $s\ge 0$ permits returning zero for every nonnegative integer input; it does not specify the intended triangular number. Conversely, an impossible precondition permits no starts, making a universal correctness claim vacuous. Check both that intended inputs are admitted and that admitted outputs express the intended task.

Specify behavior by constructing a mathematical model and defining the operations on that model. Finite sequences model a FIFO queue: insertion appends, the head is the first element, and successful deletion removes it. An axiomatic specification can then be checked against the model without requiring the implementation to use that representation.

Describe operations through laws relating their observable results, without selecting an internal representation. For an abstract data type, the laws must state the operation domains and error results as well as ordinary cases. A disjoint union can distinguish a successful value from an error with the same textual spelling.

A clause stating which parts of a program state an operation preserves. A query's returned value alone does not prohibit it from also mutating the receiver; a binary update's result equation alone does not preserve its distinct operand. Explicit frame conditions rule out these behaviors and make substitution and composition arguments possible.

An auxiliary planning fluent certifying that a safety condition has been checked for the current state in automated planning. A checking action requires facts establishing the condition and adds the certificate; the hazardous action requires that certificate.

Every action capable of invalidating the check must delete the certificate. Otherwise checking a safe configuration and then changing it could authorize an unsafe action using stale evidence. For river crossing, certify that the departure bank contains no incompatible pair, invalidate the certificate on every load, unload or crossing, and require it before sailing. This compiles a safety test into positive STRIPS preconditions when a suitable finite static compatibility relation is supplied.

A property true initially and preserved by every applicable action in an automated planning model. Mathematical induction on the plan length then proves it for every reachable state. Typical examples are unique object locations, a capacity bound, and exactly one occupancy marker being true. An invariant is a consequence to prove from the action rules; merely declaring the intended capacity in prose does not enforce it.

The condition required of a starting program state for a stated correctness guarantee. In the summation loop verification, $n\in \mathbb{Z}$ and $n\ge 0$ admit $n=0$ and $n=4$, but exclude $n=-1$. The accompanying model assumes exact integer arithmetic and terminating elementary operations. The initial values of $i,s$ need no restriction because initialization overwrites them before use.

A precondition is a logical assumption, not automatically an executable check. Writing require in a procedure states its contract; an implementation that checks or rejects invalid inputs needs that behavior specified too. Weakening a precondition admits more starts and therefore demands more proof: dropping $n\ge 0$ here makes $n=-2$ a terminating counterexample to $2s=n(n+1)$, since initialization returns zero while $n(n+1)=2$.

The condition required of a final program state when a program finishes under its precondition. The summation loop verification requires returned value $s$ to satisfy $2s=n(n+1)$ and preserves the input $n$. Relating the answer to the original input matters: allowing the program to replace $n$ by zero would change the intended contract.

A postcondition alone gives no promise of algorithm termination. It also need not specify a unique output: $s\ge 0$ allows many answers, while the exact triangular number equation determines one integer answer for each permitted $n$. Stronger postconditions express more obligations; proving only a weaker consequence cannot justify the stronger requirement.

Conformance of compiled machine code to the behaviour of the code model used to justify it. Binary correctness can extend formal verification across the compilation step; the result applies to the particular compiled artifact and its assumptions.