SPARK Prover

The SPARK Prover is the automated theorem-proving toolchain that verifies whether a SPARK program satisfies its contracts. Originally developed as a standalone verification engine in the 1980s, the modern SPARK Prover (integrated into SPARK Pro and GNATprove) translates SPARK code and annotations into verification conditions that are dispatched to automated SMT solvers, primarily Alt-Ergo. The prover attempts to establish that every precondition is satisfied at every call site, that every postcondition follows from the program body, and that no runtime error can occur on any execution path.

The SPARK Prover represents a practical compromise between the ideal of full formal verification and the reality of industrial software development. Unlike interactive proof assistants that require human guidance for every lemma, the SPARK Prover operates automatically: the programmer writes contracts, the tool generates proof obligations, and the SMT solver attempts to discharge them without human intervention. When the solver succeeds, the property is proven. When it fails, the programmer must refine the contract, add a loop invariant, or restructure the code — a feedback loop that disciplines the programmer into writing code that is not merely correct but demonstrably correct.

This approach has proven effective at scale. The SPARK Prover has been used to verify absence of runtime errors in millions of lines of flight control software, cryptographic implementations, and railway signaling systems. Yet it also reveals the limits of automation: some true properties exceed the prover's capacity, and the gap between what is true and what the prover can prove remains a source of frustration and a target of ongoing research. The SPARK Prover does not eliminate the need for human judgment; it relocates it from the act of debugging to the art of writing provable specifications.