Ada contracts versus SPARK proof: what does GNATprove verify that run-time checks do not?

A run-time check only tells you about the inputs you happened to execute. With pragma Assertion_Policy (Check), or the -gnata switch in GNAT, a false Pre or Post raises Assertion_Error at the moment it is violated; with assertions off, which is the default in GNAT, the contract is only documentation.

GNATprove instead turns the body and its contracts into logical formulas and asks automatic provers to show that they hold for every input that satisfies the precondition. Nothing is executed. A proved postcondition holds for all 4096 raw values, not just for the ones in your test set.

The second thing it proves is that none of the language-defined checks can fail: overflow, range, index, division by zero and so on. Your expression is a good example. If Raw is a plain Integer, Raw * 3300 can overflow, and the tool reports that the overflow check might fail.

Declare the parameter with subtype Raw_Type is Integer range 0 .. 4095 and the largest intermediate value is 4095 × 3300 = 13,513,500, far below the 32-bit limit of 2,147,483,647, so the check is proved without any precondition. Precise types do much of the specification work in SPARK.

What the tool needs from you: the unit must be in the SPARK subset, marked with SPARK_Mode => On. The subset excludes or restricts features that make sound analysis impractical, such as aliasing between writable parameters, side effects in ordinary functions and unrestricted access types (pointers are allowed under an ownership discipline). The exact rules have been relaxed over successive releases, so consult the SPARK reference manual for your toolchain.

Loops usually need a Loop_Invariant, and callers are verified against the contracts of what they call, not against the bodies, so a subprogram with no postcondition tells its callers nothing about its result.

Adoption is usually described in levels, and you do not need to go all the way. Stone: the code is valid SPARK. Bronze: flow analysis passes, meaning no uninitialised reads and data flows that match any Global and Depends contracts. Silver: absence of run-time errors is proved. Gold: key functional properties expressed as contracts are proved. Platinum: full functional correctness.

Silver is a common target for embedded code, because it rules out Constraint_Error failures such as overflows and out-of-range indexes for every possible input.

Proof does not replace testing; it changes what you test. A proof is relative to its assumptions: the contracts say what you meant, the hardware and compiler behave as modelled, and any code outside SPARK (drivers in C, units with SPARK_Mode => Off, anything justified with pragma Assume) honours the contracts you gave it. Timing, stack usage and whether 3300 mV really is your reference voltage are outside the proof as well.

A sensible split is to prove the computational core, keep assertions enabled while testing the boundaries where proved code meets unproved code, and test the integrated system on the target.