Verification Condition

A verification condition is a logical formula generated by a program verification tool whose validity implies that a program satisfies its specification. When a programmer writes a function with preconditions and postconditions — in WhyML, annotated C, or any other specification-carrying language — the verification toolchain applies a weakest precondition calculus or similar transformation to produce a set of formulas. If every formula is valid, the program is correct; if any formula is invalid, the counterexample points to a bug or a missing invariant.

The art of verification lies not in proving the formulas — that is the prover's job — but in ensuring that the formulas accurately capture the program's behavior. A verification condition that abstracts away pointer aliasing may be easy to prove and worthless as a guarantee. The gap between the program and its logical shadow is the central epistemic risk of all automated verification.