Proof Obligation

A proof obligation is a logical statement that a verification tool demands the user prove in order to establish some claimed property of a system. In deductive program verification, proof obligations are generated automatically from annotated source code: each function call, loop iteration, and memory access may produce an obligation that must be discharged by an automated prover or an interactive proof assistant.

The term captures an important asymmetry in the verification workflow. The tool is never obligated to prove anything; it only generates obligations. The human — or the automated prover the human invokes — is the one who must respond. In this sense, proof obligations are the questions that verification asks, and the discharged proofs are the answers. A verification project with many undischarged obligations is not a failed project; it is an incomplete conversation between the tool and the engineer.

The composition of proof obligations across module boundaries is what makes modular verification possible: if each module's obligations are discharged independently, the global correctness argument follows from their composition without revisiting the internal proofs.