Proof obligation

A proof obligation is a logical condition that must be discharged — that is, proved — in order to establish that a program, system, or mathematical construction satisfies its specification. In program verification, a proof obligation typically arises from the application of a verification calculus, such as Hoare logic or weakest precondition calculus, which breaks the correctness of a whole program into a collection of local verification conditions associated with each statement or method.

The significance of proof obligations is practical: they transform the daunting task of verifying an entire system into a modular set of lemmas that can be attacked by automated theorem provers, SMT solvers, or human proof engineers. However, a proof obligation is only as meaningful as the specification from which it is derived. A trivial proof obligation generated from a vacuous specification proves nothing. The generation of proof obligations is the engine of formal verification; their discharge is merely the fuel.