Introduction to Formal Verification with SPARK — From Ada Contracts to Mathematical Proof
· Go Komura · Ada, SPARK, Formal Verification, GNATprove, Design by Contract, High Integrity, Programming Language, High Reliability
1. Introduction — Beyond “Run It and See”
The most common way to ensure software quality is testing.
Testing: verify that the program behaves correctly for selected inputs
But testing has inherent limitations. The number of possible inputs is infinite, and testing alone cannot demonstrate correctness for all of them.
This is where formal verification comes in.
Formal verification: mathematically prove that a property holds for all possible inputs
The previous article “The Appeal of the Ada Language” gave an overview of Ada and touched briefly on SPARK.
This article focuses specifically on practical formal verification with SPARK and covers the following:
What SPARK is and its relationship to Ada
How to write contracts (Pre/Post)
How to prove them with GNATprove
How to design loop invariants
How to manage side effects with data-flow contracts (Global/Depends)
A step-by-step adoption strategy using proof levels (Stone through Platinum)
How to integrate SPARK into real projects
The goal is to let you experience the step-up from testing to proof through working code examples.
The code fragments in this article are available as a reference code collection organized by chapter on GitHub.
ada-spark-formal-verification - komurasoft-blog-samples (GitHub)
2. What Is SPARK — Ada’s Subset and Gateway to the World of Proof
SPARK is a subset of the Ada language.
Being a subset is a deliberate design choice.
Full Ada → highly expressive, but verifying everything is impractical
SPARK → restricted to verifiable features, making proof realistic
The main things SPARK restricts are:
Dynamic memory management via pointers (access types) → controlled through ownership
Free use of exception handlers → allowed in restricted form
Recursive data structures → restricted because they are hard to prove
Free use of tasking → restricted via the Ravenscar profile
“Restrictions” may sound constraining, but these restrictions are the price of provability.
The core of the SPARK toolset is GNATprove, provided by AdaCore.
How GNATprove works:
1. Analyze SPARK-annotated Ada code
2. Translate contracts (Pre/Post) and assertions into the Why3 intermediate language
3. Attempt proofs using automatic provers such as Z3, CVC4, and Alt-Ergo
4. Report results as messages on the source code
Crucially, SPARK is built on top of Ada.
SPARK code = Ada code + contract annotations
In other words, SPARK is a natural extension of everyday Ada development. There is no need to learn a completely different syntax.
3. Installing GNATprove and Your First Proof
First, let’s set up an environment to run GNATprove.
With Alire, you can create a SPARK-ready project with the following:
alr init --bin spark_demo
cd spark_demo
Since GNATprove is bundled with the GNAT compiler, if you can build with alr build, the gnatprove command is available out of the box.
As our first proof target, let’s write a function that returns the absolute value.
package Simple_Proof with SPARK_Mode is
function Abs_Value (X : Integer) return Integer
with Post => Abs_Value'Result >= 0;
end Simple_Proof;
package body Simple_Proof with SPARK_Mode is
function Abs_Value (X : Integer) return Integer is
begin
if X < 0 then
return -X;
else
return X;
end if;
end Abs_Value;
end Simple_Proof;
Key points to notice:
Add with SPARK_Mode to both the package spec and body
Declare the property "result is non-negative" as a Post condition
Use the 'Result attribute to refer to the function's return value
Now run GNATprove on this code:
gnatprove -P spark_demo.gpr
The output will be:
SUMMARY
-------
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
simple_proof.adb:5:15: info: range check proved
simple_proof.adb:6:16: info: range check proved
simple_proof.ads:3:19: info: postcondition proved
The message postcondition proved means that for all possible Integer inputs, the return value is non-negative has been mathematically proven.
This is the gateway experience of SPARK.
4. Foundations of Design by Contract — Writing Pre and Post
SPARK proofs begin with writing contracts.
Contracts are an Ada 2012 language feature, but in SPARK they become input to the proof.
procedure Transfer (From, To : in out Account; Amount : Positive)
with Pre => From.Balance >= Amount,
Post => From.Balance = From.Balance'Old - Amount
and then
To.Balance = To.Balance'Old + Amount;
Guidelines for designing Pre and Post conditions:
Pre (precondition):
The caller's responsibility
"If you call me with this condition satisfied, I guarantee the Post"
Weak enough to be satisfiable, strong enough to be useful
Post (postcondition):
The implementation's responsibility
"After the call, the world looks like this"
Use the 'Old attribute to refer to pre-call values
Too strong makes implementation too constrained; too weak proves nothing useful
Common mistakes and how to avoid them:
Mistake 1: Pre too strong
Pre => X > 0 and X < 100 and X /= 50 and ...
→ Check: can the caller always satisfy this?
→ Don't tighten Pre just because tests pass
Mistake 2: Post too weak
Post => True
→ Guarantees nothing. The proof is meaningless.
Mistake 3: Forgetting side effects in Post
Post => Result = X * 2 (missed updating a global variable)
→ Use Global/Depends contracts to make side effects explicit (Section 9)
5. Proving Freedom from Overflow — Guaranteeing Numerical Safety
One of the most practically valuable things SPARK proves is freedom from overflow.
Consider this code:
procedure Increment (X : in out Integer)
with SPARK_Mode,
Pre => X < Integer'Last,
Post => X = X'Old + 1;
Pre => X < Integer'Last is key. With this contract, GNATprove can prove the addition will not overflow.
Without a contract, GNATprove warns about possible overflow:
medium: overflow check might fail
The same applies to more complex calculations:
function Average (A, B : Integer) return Integer
with SPARK_Mode,
Pre => (if A >= 0 and B >= 0 then A <= Integer'Last - B
elsif A < 0 and B < 0 then A >= Integer'First - B),
Post => (if A <= B then A <= Average'Result and Average'Result <= B
else B <= Average'Result and Average'Result <= A);
The Pre may look complex, but it simply expresses “the sum A+B does not overflow” with sign-aware case analysis.
Takeaway:
The essence of overflow proof is declaring, in Pre, that the result of
addition or multiplication fits within the type's range
It may look tedious, but once written, you'll never suffer another overflow bug
6. Loop Invariants — Proving Properties of Loops
One of the hardest parts of formal verification is proving properties of loops.
Loops execute an arbitrary number of times, so testing cannot cover all cases. SPARK uses loop invariants for the proof.
function Sum_Of_Naturals (N : Natural) return Natural
with SPARK_Mode,
Post => Sum_Of_Naturals'Result = (N * (N + 1)) / 2;
function Sum_Of_Naturals (N : Natural) return Natural is
Result : Natural := 0;
begin
for I in 1 .. N loop
Result := Result + I;
pragma Loop_Invariant (Result = (I * (I + 1)) / 2);
end loop;
return Result;
end Sum_Of_Naturals;
Designing loop invariants requires the following mindset:
1. Write a property that holds at the start of every iteration
2. Choose one that, after the final iteration, implies the desired Post condition
3. The invariant expresses the partial computation up to that point as a formula
Here is another example: searching an array.
function Find (Arr : Array_Of_Integer; Target : Integer) return Natural
with SPARK_Mode,
Post => (if Find'Result = 0 then
(for all K in Arr'Range => Arr (K) /= Target)
else
Arr (Find'Result) = Target);
function Find (Arr : Array_Of_Integer; Target : Integer) return Natural is
begin
for I in Arr'Range loop
if Arr (I) = Target then
return I;
end if;
pragma Loop_Invariant
(for all K in Arr'First .. I => Arr (K) /= Target);
end loop;
return 0;
end Find;
The invariant here is: “in the range examined so far, Target does not exist.”
Principles for designing loop invariants:
Express as a formula: "after n iterations, what can we say?"
For array loops, the pattern is often "for the processed range, P holds"
Too strong an invariant cannot be proved; too weak won't imply the Post
Finding the right balance is where loop-proving skill is earned
7. Assertion Pragmas — Partial Properties in Code
In addition to contracts (Pre/Post), SPARK lets you write assertions within the code body.
procedure Divide (A, B : Integer; Q, R : out Integer)
with SPARK_Mode,
Pre => B /= 0,
Post => A = Q * B + R and R >= 0 and R < abs (B);
procedure Divide (A, B : Integer; Q, R : out Integer) is
begin
Q := A / B;
R := A rem B;
pragma Assert (A = Q * B + R);
pragma Assert (R >= 0);
pragma Assert (R < abs (B));
end Divide;
How to use the different pragmas:
Pre/Post: Promises at subprogram entry and exit
Assert: A property that should hold at a specific point in the code
Loop_Invariant: A property preserved across every loop iteration
Loop_Variant: A decreasing quantity to prove the loop terminates
Good places to use Assert:
Verifying intermediate results of complex calculations
Checking state after if/else branches
Confirming properties of return values after procedure calls
Providing lemmas that help subsequent proofs
8. Data-Flow Contracts — Global and Depends
One of SPARK’s powerful features is data-flow contracts.
They explicitly declare which global variables a subprogram reads and writes.
package Counter_Unit with SPARK_Mode is
Count : Natural := 0;
procedure Increment
with Global => (In_Out => Count);
procedure Reset
with Global => (Output => Count);
function Get_Value return Natural
with Global => (Input => Count);
end Counter_Unit;
Global contract modes:
Input: read-only (for functions)
Output: write-only (for initialization)
In_Out: read-write (for updates)
Furthermore, you can express dependencies between variables with Depends:
procedure Transfer
(From, To : in out Account_Type)
with Global => (Input => Exchange_Rate),
Depends => (From =>+ (From, Exchange_Rate),
To =>+ (To, Exchange_Rate));
=>+ means “depends on the previous value plus these additional inputs.”
Benefits of data-flow contracts:
1. "What does this function touch?" is obvious at a glance
2. Unintended side effects are detected at compile time
3. They feed into information-flow analysis of variables
4. They help visualize data flow in large systems
9. Proof Levels — Step-by-Step Adoption from Stone to Platinum
SPARK defines the concept of proof levels.
Trying to fully prove all code at once often leads to frustration. SPARK therefore provides a strategy of incrementally increasing proof rigor.
Stone (Level 0):
Contract syntax and type consistency checks only
The first level to reach
Bronze (Level 1):
Stone + proof of no reads of uninitialized variables
Basic correctness assurance
Silver (Level 2):
Bronze + proof of no runtime errors (bounds, overflow, division by zero)
The most practical goal
Gold (Level 3):
Silver + proof of Pre/Post conditions
Full functional correctness guarantee
Platinum (Level 4):
Gold + proof of data non-interference and information flow
For security-critical systems
A practical adoption strategy:
Phase 1: Get the entire project through Stone level
→ Catch contract writing mistakes
Phase 2: Bring critical modules to Silver level
→ Eliminate overflow and out-of-bounds access
→ Most real-world bugs are caught here
Phase 3: Prove core logic at Gold level
→ Mathematically guarantee functional correctness
→ Prove algorithm correctness
Phase 4: Go to Platinum if security requirements demand it
→ Detect information leak paths
10. A Practical Proof Workflow — Reducing Rework
Here is a workflow for using GNATprove in day-to-day development:
1. Design types and specifications
Decide range constraints and type invariants
2. Write contracts (Pre/Post)
Express the specification as contracts before implementing
3. Get it to compile
Fix compilation errors with GNAT
4. Run GNATprove at Stone level
gnatprove -P proj.gpr --level=0
5. Check warnings and refine contracts as needed
Pay special attention to initialization issues
6. Aim for Silver level
gnatprove -P proj.gpr --level=2
Eliminate all runtime errors
7. Add loop invariants where needed
If a proof fails, check whether invariants are missing
8. Prove functional correctness at Gold level
gnatprove -P proj.gpr --level=3
Common “cannot prove” situations and how to handle them:
Case 1: "medium: postcondition might fail"
→ Post condition too strong, or Pre condition too weak
→ Or insufficient loop invariants
Case 2: "medium: overflow check might fail"
→ Restrict value ranges in Pre
→ Or narrow the type's range itself
Case 3: "medium: array index check might fail"
→ Use a loop invariant to show the loop range is within the array bounds
→ Use for I in Arr'Range to help SPARK's automatic range recognition
Case 4: "prover timeout"
→ The prover timed out; break down with stepwise invariants
→ Split large functions into smaller ones
11. Using SPARK and Testing Together — Understanding the Complementary Relationship
Formal verification and testing are not adversaries; they complement each other.
SPARK proofs:
Prove properties for all possible inputs
Only cover properties written in contracts
Unprovable cases are deferred to manual review or testing
Testing:
Verify actual behavior for selected inputs
Can discover implicit assumptions not written in contracts
Can verify interaction with the runtime environment
Patterns for combined use:
1. Guarantee no runtime errors (Silver level) with SPARK
2. Verify specific input/output correctness with unit tests
3. Prove core logic at Gold level
4. Concentrate tests on parts that cannot be proved
Ada has the AUnit unit testing framework. A practical combination is: solidify types and contracts with SPARK, then test behavior with AUnit.
12. Reading GNATprove Results — Interpreting Messages
GNATprove output has three severity levels:
info: Proof succeeded
medium: Proof failed (warning). Manual review needed
high: Proof failed (error). Likely a contract violation
Common messages and their meanings:
"postcondition proved" Post condition has been proved
"range check proved" Range check has been proved
"overflow check proved" Freedom from overflow has been proved
"index check proved" Array index bounds have been proved
"divide by zero check proved" Freedom from zero division has been proved
"might fail" Could not prove
"cannot prove" Prover could not complete the proof
"prover timeout" Proof did not complete within time limit
Procedure when you encounter might fail:
1. Read the code and judge whether it can actually fail
2. If it can, fix the code
3. If it shouldn't fail, strengthen the contract (Pre / invariant)
4. If it still cannot be proved, declare it as an assumption with pragma Assume
(But note: Assume is an unproven assumption, so use with caution)
13. Integrating into Real Projects
A realistic approach to introducing SPARK into an existing project:
1. Start with new code
Don't try to SPARK-ify the entire existing codebase at once
Enable SPARK_Mode on newly written modules
2. Aim for Silver
Gold (full functional proof) is ideal, but start with Silver (no runtime errors)
Even just preventing overflow has enormous practical value
3. Write contracts starting from interfaces
Write contracts in the package spec (.ads) before implementation
With a solid spec, any implementer can write code that satisfies the contracts
4. Integrate into CI/CD
Add gnatprove to the CI pipeline
Stop the build (or at least warn) on proof failure
5. Accumulate proof reports
Generate reports with gnatprove --report=all
Track the trend of unproven items over time
For projects with mixed C/C++ and Ada code, a phased approach is effective:
1. Write new modules in Ada/SPARK
2. Interface with C/C++ via Interfaces.C
3. Migrate critical data structures and verification logic to SPARK
4. Gradually expand SPARK coverage
14. SPARK’s Limitations and Cautions
SPARK is not a silver bullet. Honestly understanding its limits leads to correct application.
What SPARK can prove:
SPARK proves only the properties written in contracts
Omitted properties (things you forgot to write) are not proved
Example: proving Post that the result is sorted does not guarantee
that the original elements are preserved unless you also write that
Prover limitations:
Some complex properties exceed what automatic provers can handle
In those cases, interactive proof (Coq, etc.) is needed
That said, automatic proving suffices for most practical cases
Language restrictions:
Code heavy on pointers cannot be SPARK-ified
Proof of dynamic memory allocation is limited
Proof of recursive data structures is challenging
Developer proficiency:
Writing contracts requires practice
Designing loop invariants is especially time-consuming to learn
A team-wide upskilling plan is essential
15. Conclusion — Making Proof Part of Daily Development
We have walked through the practice of formal verification with SPARK.
SPARK is a subset of Ada, narrowed to verifiable features
Contracts (Pre/Post) are the input to proofs. Ada 2012 contracts work directly
GNATprove runs automatic proofs and reports results at the source-code level
Loop invariants prove properties of loops
Global/Depends make data flow explicit and manage side effects
Proof levels (Stone through Platinum) let you increase rigor step by step
Aiming for Silver level (no runtime errors) first is the practical recommendation
Testing and proofs are not opposites — they complement each other
You may have the preconception that “formal verification is too hard and only for special projects.”
But today’s SPARK + GNATprove combination has reached the following level:
1. Write a contract. This is fundamentally the same design activity as writing types or tests
2. Run gnatprove. It feels like compilation
3. Look at the results and fix either the code or the contract
This cycle is no different from the daily development flow of fixing code while reading compiler error messages.
The difference is: while a compiler guarantees “the syntax is correct,” GNATprove guarantees “correct for all inputs.”
The Ada catchphrase introduced in the previous article — “bugs are not things you find; types and contracts make them impossible to write” — advances to the next level with SPARK:
The absence of bugs is guaranteed by proof.
Start by adding SPARK_Mode and a Post to a small function, then run gnatprove.
When you see the green postcondition proved message, your perspective on software quality assurance will change.
References
- Reference code collection organized by chapter - komurasoft-blog-samples (GitHub)
- SPARK - AdaCore
- Introduction to SPARK - learn.adacore.com
- SPARK 2014 Reference Manual
- GNATprove User’s Guide
- Ada Reference Manual (Ada 2022)
- Alire - Ada Library Repository
- Why3 - Platform for Deductive Program Verification
- The Appeal of the Ada Language - This Site
Related Articles
Recent articles sharing the same tags. Deepen your understanding with closely related topics.
The Appeal of the Ada Language — Expressing Design Through Types and Powering Software That Runs for Decades
An introduction to the appeal of the Ada language: strong typing, range constraints, separation of specification and implementation via p...
Generic Programming in Ada — Contracts, Types, and Zero-Cost Reuse
A systematic introduction to generic programming in Ada. Covers generic subprograms, generic packages, formal subprogram parameters, type...
Safe Concurrency with Ada — A Practical Guide to Tasks and Protected Objects
A practical introduction to Ada's built-in concurrency model — tasks, rendezvous, and protected objects. Covers the rendezvous pattern (e...
Real-Time Systems Programming in Ada — Priorities, Periodic Execution, and CPU Time Control in Practice
A practical deep dive into Ada's Annex D real-time features — task priorities, the Ceiling_Locking protocol, drift-free periodic executio...
Fable Is Gone — Don't Give Up: OpenRouter Fusion + Chinese LLMs + Review Layer
Fable is nowhere near replaceable. But combine OpenRouter Fusion with 5 Chinese LLMs, then add a review layer (GPT-5.5-Pro or Codex PR re...
Related Topics
These topic pages place the article in a broader service and decision context.
Windows Technical Topics
Topic hub for KomuraSoft LLC's Windows development, investigation, and legacy-asset articles.
Author Profile
Profile page for the article author.
Go Komura
Representative of KomuraSoft LLC
Focused on Windows software development, technical consulting, and investigations into failures that are difficult to reproduce.
Public links