Proving AI-Written Code with SPARK ── Humans Write the Contracts, GNATprove Checks Them

When you have AI write a function, tests with ordinary values usually pass. The trouble is code that fails on inputs nobody wrote tests for, such as values near the integer limits or empty arrays. SPARK’s GNATprove checks, for every input that satisfies the precondition, that no run-time errors occur and that the postcondition holds. You do not have to choose test inputs.

In this article we take three small functions, assumed to have been written by AI, add preconditions (Pre) and postconditions (Post), and run them through GNATprove. Using real output, I show how to read and act on the messages when a proof fails, and separate what a proof guarantees from what it does not. Finally, I summarize what a person should read when reviewing AI-written code.

The basics of SPARK and GNATprove (installation, proof levels, data flow contracts and so on) are explained in “Introduction to Formal Verification with SPARK”. This article does not repeat them.

All examples were run on Linux (x86_64). For proofs I used gnatprove 15.1.0-1 from the GNAT FSF build (--version shows FSF 15.0; the bundled provers are Alt-Ergo 2.6.0, cvc5 1.2.1 and Z3 4.13.4), and for execution GNAT 13.3.0. Unless stated otherwise, the command is gnatprove -P p.gpr --level=2 --report=fail.

Humans Write the Contracts, AI Writes the Body

In the approach this article takes, a person writes the contracts in the function’s specification (.ads), and AI writes the body (.adb). If GNATprove reports a failure, the messages are passed to the AI so it fixes the body. Once the proof passes, the person rereads the contracts rather than the body.

flowchart TB
        accTitle: Division of work between contracts and body
        accDescr: A person writes the preconditions and postconditions, AI writes the body, GNATprove proves it; on failure the messages are passed back for a fix, and once it passes the person rereads the contracts.
        A["A person writes Pre and Post"] --> B["AI writes the body"]
        B --> C["Prove with GNATprove"]
        C -->|"Failure"| D["Pass the messages to the AI"]
        D --> B
        C -->|"Everything proved"| E["The person rereads the contracts"]

Figure 1: A person writes the contracts, AI writes the body, and GNATprove’s results drive the fixes.

The reason for this division is that a proof checks only that “the body satisfies the contract.” Whether the contract correctly expresses the specification is something only a person can judge. A later section shows an example in which a proof passes with a weak contract. AdaCore’s documentation also describes an approach in which the person who defines the specification (the low-level requirements) is separate from the person who writes the corresponding body¹.

In the diagram a solid line marks a relation that always holds and a dashed line marks a conditional one (the conditions are given per relation on the detail page). The full list of relations (12 in total, with evidence and certainty) and the definitions of the main concepts are collected on the knowledge map detail page (in Japanese). Data: JSON-LD / Turtle

Example 1: The Average of Two Integers

The first example is a function that returns the average of two Integer values. The postcondition requires the result to lie between the two values.

package Averages with SPARK_Mode is

   function Average (A, B : Integer) return Integer
     with Post => Average'Result in Integer'Min (A, B) .. Integer'Max (A, B);

end Averages;

Overflow in the Addition

Suppose the first body the AI wrote is the following expression.

package body Averages with SPARK_Mode is

   function Average (A, B : Integer) return Integer is
   begin
      return (A + B) / 2;
   end Average;

end Averages;

GNATprove’s output is as follows.

averages.adb:5:17: high: overflow check might fail, cannot prove lower bound for (A + B)
    5 |      return (A + B) / 2;
      |             ~~~^~~~
  e.g. when A = Integer'First
        and B = -1
  reason for check: result of addition must fit in a 32-bits machine integer
  possible fix: add precondition (if B >= 0 then A <= Integer'Last - B else A >= Integer'First - B) to subprogram at averages.ads:3
    3 |   function Average (A, B : Integer) return Integer
      |            ^ here

The first line gives the file, line and column, the severity (high), the kind of check (overflow check), and why it could not be proved. The e.g. when lines are a counterexample: when A = Integer'First and B = -1, A + B falls below the range of Integer. possible fix is a suggested precondition that would make the proof pass.

flowchart TB
        accTitle: How to read a GNATprove failure message
        accDescr: The first line of a failure message gives the location, severity and kind of check; the counterexample lines give an example input that fails; the reason line gives what the check is; the suggestion line gives a precondition that would make the proof pass.
        A["First line: location, severity, kind of check"] --> B["e.g. when: counterexample values"]
        B --> C["reason for check: what the check is"]
        C --> D["possible fix: suggested precondition"]
        B -.-> E["Run with the counterexample values to confirm"]

Figure 2: A failure message lists the location, the counterexample, the reason and the suggestion, in that order.

You can confirm whether a counterexample really shows a bug by running the code with those values. I built it with GNAT 13.3.0 and -gnata, which enables assertions, and called it with (2, 8), (-7, 3), (Integer'Last, Integer'Last) and (Integer'First, -1) in that order.

 5
-2

raised CONSTRAINT_ERROR : averages.adb:5 overflow check failed

The two ordinary calls were correct, and the third call raised Constraint_Error. In Ada, this exception is raised when Overflow_Check, which checks whether a value fits in the base range of its type, fails². A test with only ordinary values would pass this body.

According to AdaCore’s documentation, a counterexample does not necessarily correspond to an input that can actually run. The severity of a message can also be raised from medium to high as a result of checking the counterexample³. When I proved the same body with --level=1, the severity was medium and there was no e.g. line.

The Overflow Moves to the Subtraction

Next, suppose the AI rewrote it as A + (B - A) / 2 to avoid overflow. This form assumes A <= B, so we add a precondition as well.

   function Average (A, B : Integer) return Integer
     with Pre  => A <= B,
          Post => Average'Result in A .. B;

The body is return A + (B - A) / 2;. The result is as follows; this time the subtraction overflows.

averages.adb:5:21: high: overflow check might fail, cannot prove upper bound for (B - A)
    5 |      return A + (B - A) / 2;
      |                 ~~~^~~~
  e.g. when A = Integer'First
        and B = 0
  reason for check: result of subtraction must fit in a 32-bits machine integer

Even with A <= B, if A is Integer'First and B is 0 or greater, B - A exceeds Integer'Last. Changing the addition into a subtraction only moved the overflowing inputs to a different range.

Splitting the Cases by Sign

If you use subtraction when the signs are the same and addition when they differ, neither overflows. As with the first body, there is no precondition.

package body Averages with SPARK_Mode is

   function Average (A, B : Integer) return Integer is
   begin
      if (A >= 0) = (B >= 0) then
         --  Same sign, so B - A fits in Integer
         return A + (B - A) / 2;
      else
         --  Different signs, so A + B fits in Integer
         return (A + B) / 2;
      end if;
   end Average;

end Averages;

With this body, the output of --report=fail was empty. With --report=all, the checks that were proved are also shown, one per line.

A body that adds in Long_Long_Integer (64 bits with GNAT in this environment) and then divides by 2 was likewise fully proved.

   function Average (A, B : Integer) return Integer is
      Sum : constant Long_Long_Integer :=
        Long_Long_Integer (A) + Long_Long_Integer (B);
   begin
      return Integer (Sum / 2);
   end Average;

flowchart TB
        accTitle: Three bodies of the average function
        accDescr: The body that divides A plus B by 2 overflows in the addition, the body that adds half the difference of B and A to A overflows in the subtraction, and the body that splits cases by sign was fully proved.
        A["(A + B) / 2"] --> R1["The addition overflows"]
        B["A + (B - A) / 2"] --> R2["The subtraction overflows"]
        C["Split the cases by sign"] --> R3["Everything proved"]
        R1 -.-> N1["Counterexample A = Integer'First, B = -1"]
        R2 -.-> N2["Counterexample A = Integer'First, B = 0"]

Figure 3: Three bodies of the average function and GNATprove’s results.

Adding the Suggested Precondition

If you add the possible fix precondition to the first body as it is, the proof passes. However, the inputs the function accepts become narrower. Average (Integer'First, -1) becomes a contract violation, and callers now have to show that they never pass such values.

If the goal is only to make the proof pass, the AI may add a precondition instead of fixing the body. Whether that is acceptable as a specification depends on what values the function receives, and a proof tool cannot decide that.

flowchart TB
        accTitle: Two ways to fix a failure
        accDescr: When a proof fails, adding a precondition narrows the accepted inputs and moves the condition to the caller, while fixing the body lets it be proved while still accepting every input.
        A["The overflow check fails"] --> B["Add a precondition"]
        A --> C["Fix the body"]
        B --> D["The accepted inputs narrow"]
        D --> E["Callers must respect the condition"]
        C --> F["Every input is accepted"]

Figure 4: Adding a precondition moves the responsibility for the condition to the caller.

Example 2: Clamp, Keeping a Value Within a Range

The second example is a function that keeps X within Lo to Hi inclusive. Suppose we had the AI write the contract too, and it returned the following postcondition.

package Clamps with SPARK_Mode is

   function Clamp (X, Lo, Hi : Integer) return Integer
     with Pre  => Lo <= Hi,
          Post => Clamp'Result in Lo .. Hi;

end Clamps;

If the body is return Integer'Max (Lo, Integer'Min (X, Hi));, everything is proved.

A Bug That Passes with a Weak Postcondition

This postcondition requires only that the result be within the range. Even when I changed the body to return Lo;, everything was still proved (I wrote pragma Unreferenced (X, Hi); to silence the warnings about X and Hi being unused).

Running this body with Clamp (5, 0, 10), Clamp (-3, 0, 10) and Clamp (42, 0, 10) returned 0 every time. A test with concrete expected values would fail immediately.

Rewrite the postcondition so that it determines a single result.

   function Clamp (X, Lo, Hi : Integer) return Integer
     with Pre  => Lo <= Hi,
          Post => Clamp'Result =
                    (if X < Lo then Lo
                     elsif X > Hi then Hi
                     else X);

With this contract, the return Lo; body cannot be proved, and a counterexample is shown.

clamps.ads:5:19: high: postcondition might fail
    5>|          Post => Clamp'Result =
  ... | ...
    8 |                     else X);
  e.g. when Clamp'Result = 0
        and Hi = 1
        and Lo = 0
        and X = 1

The body using Integer'Max and Integer'Min was fully proved with this contract as well. Its results are 5, 0 and 10.

flowchart TB
        accTitle: Strength of the postcondition and the proof result
        accDescr: With a postcondition that only requires the result to be within the range, even a body that always returns Lo is proved; with a postcondition that determines a single result, the proof of that body fails.
        A["Body: always returns Lo"] --> B["Post: result is in Lo..Hi"]
        A --> C["Post: determines a single result"]
        B --> D["The proof passes"]
        C --> E["The postcondition proof fails"]

Figure 5: For the same wrong body, the result depends on how strong the postcondition is.

The same is true of the average example. The body that splits by sign and the body that adds in 64 bits were both proved. Even so, the result of Average (Integer'First, -1) is -1073741825 for the former and -1073741824 for the latter; they do not match. Because the postcondition says only “between the two values,” rounding either way satisfies the contract. Which way to round is a question of specification, and a person has to decide it.

When There Is No Precondition

If you keep the first postcondition and remove Pre => Lo <= Hi, the postcondition cannot be proved even for the correct body. The counterexample is Lo = 1, Hi = 0: the range is empty, so no returned value can be within Lo .. Hi.

When this function is called from code that SPARK does not analyze, the caller’s respecting the precondition is treated as an assumption of the proof⁴. With GNAT, -gnata makes preconditions and postconditions checked at run time as well; without it they are not checked⁵. When I actually called Clamp (5, 10, 0), it raised Assertion_Error with failed precondition from clamps.ads:4 when built with -gnata, and returned 10 without it.

Example 3: Searching an Array and Loop Invariants

The third example is a function that searches an array for Key and returns its position, or 0 if it is not found.

package Search with SPARK_Mode is

   type Int_Array is array (Positive range <>) of Integer;

   --  Returns the position of Key, or 0 if it is not found.
   function Find (A : Int_Array; Key : Integer) return Natural
     with Post =>
       (if Find'Result = 0 then
          (for all I in A'Range => A (I) /= Key)
        else
          Find'Result in A'Range and then A (Find'Result) = Key);

end Search;

The body the AI wrote compares elements from the start with a for loop.

package body Search with SPARK_Mode is

   function Find (A : Int_Array; Key : Integer) return Natural is
   begin
      for I in A'Range loop
         if A (I) = Key then
            return I;
         end if;
      end loop;
      return 0;
   end Find;

end Search;

A for Loop Without an Invariant

This body is correct, yet the postcondition for the not-found case cannot be proved.

search.ads:9:36: medium: postcondition might fail, cannot prove A (I) /= Key
    9 |          (for all I in A'Range => A (I) /= Key)
      |                                   ^~~~~~~~~~~~

This time there is no counterexample. The prover does not know what holds when the loop ends, so it cannot conclude that “no element is Key.” AdaCore’s documentation lists, as causes of unproved checks, missing annotations such as loop invariants and prover timeouts, in addition to errors in the code⁶. might fail is not a definite statement that there is a bug.

At the end of each iteration, write a loop invariant saying “the elements so far are not Key.”

      for I in A'Range loop
         if A (I) = Key then
            return I;
         end if;
         pragma Loop_Invariant (for all J in A'First .. I => A (J) /= Key);
      end loop;

GNATprove checks that the loop invariant holds in the first iteration and that, if it held in the previous iteration, it also holds in the next⁷. With this, the postcondition was proved too. Searching (10, 20, 30, 20) for 20 and 99, and searching an empty array for 1, gave 2, 0 and 0.

flowchart TB
        accTitle: Loop invariants and the postcondition
        accDescr: Without a loop invariant the postcondition for the not-found case cannot be proved; writing the invariant that the elements so far are not Key lets the postcondition be proved as well.
        A["Compare from the start in a for loop"] --> B["No invariant"]
        A --> C["With an invariant"]
        B --> D["Post for the not-found case is unproved"]
        C --> E["Each iteration: elements so far are not Key"]
        E --> F["Post is proved as well"]

Figure 6: A loop invariant tells the prover what holds after the loop.

Writing It with a while Loop

When I wrote the same search with a while loop that advances the index by hand, three messages appeared.

   function Find (A : Int_Array; Key : Integer) return Natural is
      I : Positive := A'First;
   begin
      while I <= A'Last loop
         pragma Loop_Invariant (I in A'Range);
         pragma Loop_Invariant (for all J in A'First .. I - 1 => A (J) /= Key);
         if A (I) = Key then
            return I;
         end if;
         I := I + 1;
      end loop;
      return 0;
   end Find;

search.adb:4:24: medium: range check might fail, cannot prove lower bound for A'First
    4 |      I : Positive := A'First;
      |                      ~^~~~~~
  reason for check: default component value must fit in the type

search.adb:6:25: medium: implicit aspect Always_Terminates on "Find" could be incorrect, loop might be nonterminating
    6 |      while I <= A'Last loop
      |                        ^~~~
  possible fix: add loop variant in the loop body

search.adb:12:17: medium: overflow check might fail, cannot prove upper bound for I + 1
   12 |         I := I + 1;
      |              ~~^~~
  reason for check: result of addition must fit in a 32-bits machine integer

The first is about the lower bound of an empty array. In Ada, an empty range does not have to lie within the range of the index type⁸. So A'First of an empty array is not necessarily within Positive. The third points out that for an array whose A'Last is Integer'Last, I + 1 overflows after the last element has been examined. The second says it cannot show that the loop terminates. By default, GNATprove also checks that functions always terminate⁹.

With a for loop, the language determines the range of the index, so none of these three appeared.

What a Proof Guarantees and What It Does Not

Let’s sum up the results so far. When GNATprove says “everything proved,” what has been checked is that, for every input satisfying the precondition, the body within SPARK raises no run-time error and the postcondition holds. It is not the result of selected inputs, as in testing.

On the other hand, it does not check the following.

• Whether the contract matches the specification. The weak postcondition of Clamp and the rounding in the average example are cases in point.
• Whether code that SPARK does not analyze respects the contracts. That callers respect the precondition, and that callees behave according to their contracts, are treated as assumptions⁴.
• Things a person has declared to hold. pragma Assume and pragma Annotate in the next section are cases in point.
• Running out of memory. AdaCore’s documentation lists the sizes of the stack and the heap as assumptions to be checked separately⁴.

flowchart TB
        accTitle: What a proof checks
        accDescr: GNATprove checks that the body satisfies the contract and that no run-time errors occur; it does not check whether the contract matches the specification, code outside the analysis, what was declared with Assume or Annotate, or running out of memory.
        A["GNATprove's proof"] --> B["Checks"]
        A --> C["Does not check"]
        B --> D["No run-time errors occur"]
        D ~~~ E["The body satisfies Post"]
        C --> F["Whether the contract matches the spec"]
        F ~~~ G["Code outside the analysis"]
        G ~~~ H["What Assume and Annotate declare"]
        H ~~~ I["Running out of memory"]

Figure 7: What a proof checks, and what it treats as assumptions.

Ways of Making Proof Failures Disappear from the Output

A failed proof can be made to disappear from the output without fixing the code. When you have only asked an AI to “get rid of the GNATprove errors,” check whether lines like these have entered the diff. I tried three ways on the first body, (A + B) / 2.

pragma Assume

When I wrote pragma Assume (A in -1_000 .. 1_000 and B in -1_000 .. 1_000); at the start of the body, the --report=fail output was empty. pragma Assume is a pragma that makes GNATprove use a property as true in the rest of the analysis without checking it⁷. However, gnatprove.out records where it was used.

  Averages.Average at averages.ads:3 flow analyzed (0 errors, 0 checks, 0 warnings and 1 pragma Assume statements) and proved (3 checks)
   pragma Assume statements:
    averages.adb:5:7

Justification with pragma Annotate

pragma Annotate (GNATprove, False_Positive, "overflow check might fail", "reason") justifies a check message as a “false positive.” This pragma applies to the preceding item. When I first placed it before the return statement, I got a warning that there was nothing to justify, and the overflow message remained. When I moved the addition into a constant declaration and placed the pragma right after it, the message changed to info: overflow check justified¹⁰. In the gnatprove.out table it is counted as 1 in the Justified column, and the reason string is recorded too.

   Justified check messages:
    averages.adb:4:35: overflow check justified (marked as: false positive, reason: "A and B only take small values")

SPARK_Mode => Off

When the body is declared as package body Averages with SPARK_Mode => Off is, the body is not analyzed. The only output was warning: no checks generated by GNATprove, and gnatprove.out recorded skipped; body is SPARK_Mode => Off.

AdaCore’s documentation says that all justifications of check messages should be reviewed, and that justifications through pragma Assume should be examined carefully⁴. There are situations in which each of the three has a legitimate use. The problem is when they enter the diff without anyone confirming the reason.

flowchart TB
        accTitle: Three ways of making proof failures disappear from the output
        accDescr: pragma Assume is used as an assumption, pragma Annotate is counted as justified, and SPARK_Mode Off stops the body from being analyzed; each leaves a record in gnatprove.out.
        A["A failed check"] --> B["pragma Assume"]
        A --> C["pragma Annotate"]
        A --> D["SPARK_Mode => Off"]
        B --> E["The location of the Assume is recorded"]
        C --> F["Counted as Justified"]
        D --> G["Recorded as skipped"]

Figure 8: Whichever way is used, it leaves a trace in gnatprove.out.

What People Look At in a Review

When you run GNATprove on AI-written code, a person should read in the following order.

1. Preconditions. Check that they do not shut out inputs the business will send, and that they are not conditions added only to make the proof pass, like the possible fix in the average example.
2. Postconditions. Check whether they determine a single result, and if not, whether the remaining latitude (such as rounding) is allowed by the specification.
3. Any pragma Assume, pragma Annotate or SPARK_Mode => Off in the diff. Check that each has a reason.
4. The gnatprove.out table. Check that Unproved is 0, and look at the number of Justified entries with their reasons and the list of pragma Assume statements.

Reading the body line by line can come after that. If the contracts match the specification and everything is proved without assumptions, the body neither raises run-time errors nor violates the postcondition.

flowchart TB
        accTitle: The order for reviewing AI-written code
        accDescr: Check the preconditions, the postconditions, any added Assume, Annotate or SPARK_Mode Off, and the gnatprove.out table, in that order, and read the body after that.
        A["Pre: does it shut out inputs?"] --> B["Post: is the result determined?"]
        B --> C["Reasons for Assume, Annotate and Off"]
        C --> D["Counts of Unproved and Justified"]
        D --> E["Read the body"]

Figure 9: Read the contracts and the proof results before the body.

Combining with Tests

AdaCore’s documentation says that properties that have been proved do not need to be tested, and that unit tests can be reduced or even eliminated¹. That holds, however, only when the contracts correctly express the requirements. If you have AI write the contracts too, tests remain as a way of checking that the contracts match the requirements. The bug that passed the proof with Clamp’s weak postcondition was one you would find immediately by running concrete values and comparing them with expected values. Conversely, the overflow at extreme values, which ordinary values never trigger, was found by the proof.

A postcondition states a property that holds for any input, so it has the same shape as a property in property-based testing. The difference is that a test tries many inputs, while a proof checks every input. How to judge tests written by AI, and how to examine the weaknesses of tests with tools, are covered in the following articles.

• Can You Trust Tests Written by AI?
• Finding Untested Code with Coverage
• Testing Your Tests with Mutation Testing
• Property-Based Testing: Trying the Inputs Examples Never Reach

If you want to check tools or macros your staff built with generative AI before using them in production, we take consultations through “Professional Review of AI-Written Code”.

Related Articles

• Introduction to Formal Verification with SPARK — From Ada Contracts to Mathematical Proof
• The Appeal of the Ada Language — Expressing Design Through Types and Powering Software That Runs for Decades
• Connecting Ada with C and C# — Building a DLL and Calling It
• Starting an Ada Project with Alire

References

Related Articles

Recent articles sharing the same tags. Deepen your understanding with closely related topics.

Related Topics

These are topic pages close to this theme. Starting from the article, you can go on to related services and other articles.

Services Connected to This Topic

This article leads to the following service pages. Start from the entry point closest to your situation.

Frequently Asked Questions

Questions commonly asked at the time of consultation about the topic of this article.

What do you learn when you run GNATprove on Ada code written by AI?

For code written within SPARK, it checks, for every input that satisfies the precondition, that no run-time errors such as overflow or out-of-range array access occur and that the postcondition holds. Anything it cannot prove is reported with the line and column, the reason, and counterexample values.

If GNATprove's proof passes, is a review still needed?

Yes. A proof checks that the body satisfies the contract; it does not check that the contract matches the specification. If the postcondition is weak, even a wrong body passes the proof. Rather than the body, people read the preconditions and postconditions and any added pragma Assume, pragma Annotate or SPARK_Mode => Off.

When GNATprove says "might fail", is the code always wrong?

Not always. Besides cases where the code is wrong, it also appears when annotations such as loop invariants are missing, or when the prover cannot complete the proof in time. If counterexample values are shown, checking whether the code actually goes wrong with those values helps narrow down the cause.

Can I simply add the precondition that GNATprove suggests?

The proof will pass, but the inputs the function accepts become narrower. Meeting the condition becomes the caller's responsibility, so a person has to decide whether the condition covers every input the business can produce. If it does not, fix the body instead.

Author Profile

Profile page for the article author.

Go Komura

Representative of KomuraSoft LLC

Focused on Windows software development, technical consulting, and bug investigation, with particular strength in projects where existing assets remain and in investigating failures whose cause is hard to see.