# SPARK within CI **URL:** \ **Category:** General\ **Tags:** spark, ci\ **Created:** [October 23, 2026, 1:25pm UTC](https://forum.ada-lang.io/t/spark-within-ci/4888 "2026-10-23T13:25:54Z")\ **Posts on this page:** 12\ **Page:** 1
**Author:** ![LionelDraghi](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/lioneldraghi/32/416_2.png) [@LionelDraghi](https://forum.ada-lang.io/u/LionelDraghi)\ **Post date:** [October 23, 2026, 1:25pm UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/1 "2026-10-23T13:25:54Z")
I’ve recently started a project involving several firsts for me, including SPARK. GNATprove already takes much longer than the test suite, and I expect the gap to grow as the project gets larger. My GitHub CI ([topoproof/.github/workflows/ci.yml at 549bf2f9ad1fcb1b325aa4a2fe1777fc86ba5dc2 · LionelDraghi/topoproof · GitHub](https://github.com/LionelDraghi/topoproof/blob/549bf2f9ad1fcb1b325aa4a2fe1777fc86ba5dc2/.github/workflows/ci.yml)) has two jobs, **build and test** and **prove** , both currently running on Linux, macOS, and Windows. This feels like a lot of potentially unnecessary CI usage. My assumption is that proofs are platform-independent, so running GNATprove on just one platform should be enough. Is that assumption too naive? How do you handle SPARK proofs in your CI? ---
**Author:** ![pyj](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/pyj/32/5_2.png) [@pyj](https://forum.ada-lang.io/u/pyj)\ **Post date:** [October 23, 2026, 1:52pm UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/2 "2026-10-23T13:52:45Z")
At every point in a proved project I’ve done, I’ve had to analyze which proofs take the most number of steps and then optimize them. There’s a `gnatprove` option to get what you want. ---
**Author:** ![bladeacer](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/bladeacer/32/1018_2.png) [@bladeacer](https://forum.ada-lang.io/u/bladeacer)\ **Post date:** [October 23, 2026, 11:26pm UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/3 "2026-10-23T23:26:09Z")
Proving between platforms on the same piece of code should behave the same, though I would advise at least building and testing on each release for macOS and Windows (I was able to uncover some hard coded UNIX paths in my code as a result). Shameless plug but you might find my project useful, especially as your codebase grows (there’s certain niceties like spark proof coverage, status badges, dashboard etc). There is some work being done on caching gnatprove in CI for my GitHub Action, though it is more rudimentary compared to the base CLI in that regard for now. Repo: [GitHub - bladeacer/adacovex: Ada/SPARK formal verification and compliance toolchain. · GitHub](https://github.com/bladeacer/adacovex) ---
**Author:** ![docandrew](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/docandrew/32/396_2.png) [@docandrew](https://forum.ada-lang.io/u/docandrew)\ **Post date:** [October 23, 2026, 11:30pm UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/4 "2026-10-23T23:30:27Z")
I typically skip proofs in CI for this reason - most hosted runners just aren’t beefy enough to prove in a reasonable timeframe. One option is to just report the successful proof, something like: ```bash gh api \ --method POST --silent \ -H "Accept: application/vnd.github+json" -H "X-GitHub-Api-Version: 2022-11-28" \ /repos/$OWNER/$REPO/statuses/$SHA \ -f "context=signoff" -f "state=success" -f "description=Signed off by $USER ($SECONDS seconds)" ``` but instead of “Signed off by” you could add some kind of digitally-signed artifact, a hash of the gnatprove output, perhaps, depending on your paranoia level. ---
**Author:** ![bladeacer](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/bladeacer/32/1018_2.png) [@bladeacer](https://forum.ada-lang.io/u/bladeacer)\ **Post date:** [October 23, 2026, 11:37pm UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/5 "2026-10-23T23:37:14Z")
Or if you wish to skip running gnatprove in CI entirely, you can always run gnatprove and commit the gnatprove.out, which can one can read from directly. Albeit running gnatprove on one’s local machine for every git push is still not a computationally “cheap” gate. I feel doing it on every release gives you a sensible balance there, as it reassures users while you can run gnatprove for local development. ---
**Author:** ![JC001](https://forum.ada-lang.io/letter_avatar_proxy/v4/letter/j/e56c9b/32.png) [@JC001](https://forum.ada-lang.io/u/JC001)\ **Post date:** [October 24, 2026, 10:03am UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/6 "2026-10-24T10:03:00Z")
> [@LionelDraghi](#): > > proofs are platform-independent This is not entirely true. Before SPARK 14, one had to tell the prover what the sizes of the predefined numeric types and the`System.Min_Int`, `System.Max_Int`, and `System.Max_*_Modulus` constants were to get meaningful proofs for a specific platform; something that could be proved for one platform might fail on another. So for a single proof to apply to all platforms, you have to ensure that all your numeric types have fixed sizes, regardless of platform. Effectively that means no use of the `Long_*` predefined types, or types declared using the `System` constants. ---
**Author:** ![ksson](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/ksson/32/1082_2.png) [@ksson](https://forum.ada-lang.io/u/ksson)\ **Post date:** [October 24, 2026, 10:55am UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/7 "2026-10-24T10:55:38Z")
Technically, proofs can differ between those three platforms. There can be differences in the runtime, or in sizes of some predefined types. But it can be mitigated and overall it’s quite rare. For CI use, I would suggest the use of a “file cache”. This feature is hidden behind the option `—memcached-server=file:path`, where “file” is a fixed string and “path” is a path on disk (yes the name is a bit awkward; no memcached server is needed for this feature). Gnatprove then saves proof results in that folder. If you save and restore it for the next CI run (typically CI have this feature to restore a cache folder), you should see important speedups. ---
**Author:** ![LionelDraghi](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/lioneldraghi/32/416_2.png) [@LionelDraghi](https://forum.ada-lang.io/u/LionelDraghi)\ **Post date:** [October 24, 2026, 2:58pm UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/8 "2026-10-24T14:58:04Z")
Thanks for the tip, very effective indeed! | `prove` job | Cold (first run / no cache) | Warm (cache restored) | Speedup | | --- | --- | --- | --- | | ubuntu-latest | 18.5 min | 0.6 min | ~30× | | macos-latest | 19.0 min | 1.3 min | ~15× | | windows-latest | 13.5 min (cache disabled — gnatprove bug, worked around) | — | — | Cold runs show a variance I can’t explain (yesterday’s times were around 8 min), but nevertheless the gain is spectacular! ---
**Author:** ![LionelDraghi](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/lioneldraghi/32/416_2.png) [@LionelDraghi](https://forum.ada-lang.io/u/LionelDraghi)\ **Post date:** [October 24, 2026, 3:04pm UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/9 "2026-10-24T15:04:42Z")
I added a `make prove-stats` target (wrapping `gnatprove --report=statistics` for exactly that purpose). Here are the most difficult proved checks: | Check | Result | | --- | --- | | `topoproof-geometry-intersections.adb:390:7` | precondition proved in max 19 s | | `topoproof-geometry-intersections.adb:382:13` | overflow check proved in max 18 s | | `topoproof-geometry-segment_sequences.adb:209:17` | loop invariant after first iteration proved in max 16 s | | `topoproof-geometry-intersections.adb:331:38` | overflow check proved in max 11 s | | `topoproof-geometry-intersections.adb:334:38` | overflow check proved in max 10 s | | `topoproof-geometry-intersections.adb:352:12` | overflow check proved in max 10 s | | `topoproof-geometry-intersections.adb:357:12` | overflow check proved in max 7 s | | `topoproof-geometry-intersections.adb:82:10` | postcondition proved in max 7 s | | `topoproof-geometry-intersections.adb:383:22` | overflow check proved in max 7 s | | `topoproof-geometry-intersections.adb:768:10` | postcondition proved in max 5 s | Max steps used for a successful proof: 81,857. No single step stands out spectacularly for now — the hardest checks are the overflow checks in the intersections module, which is expected given the amount of arithmetic there. I’ll keep an eye on it as the kernel grows. Thanks for the advice, Paul. ---
**Author:** ![pyj](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/pyj/32/5_2.png) [@pyj](https://forum.ada-lang.io/u/pyj)\ **Post date:** [October 24, 2026, 3:46pm UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/10 "2026-10-24T15:46:11Z")
I’ved knocked out a lot of steps by allowing shortcuts via proving more in long chains, instead of relying on implicitly deduced intermediary results (adidng pre/post, or adding Assert, or Assert\_And\_Cut). In my limited experience doing this, 82k steps is more than 10x what I normally see. ---
**Author:** ![kevlar700](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/kevlar700/32/1118_2.png) [@kevlar700](https://forum.ada-lang.io/u/kevlar700)\ **Post date:** [October 24, 2026, 8:11pm UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/11 "2026-10-24T20:11:51Z")
> [@JC001](#): > > Effectively that means no use of the `Long_*` predefined types, or types declared using the `System` constants. A saving grace is that it is easier to prove SPARK with the use of smaller integers and the occasional use of e.g. Unsigned\_64 as a working integer. ---
**Author:** ![LionelDraghi](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/lioneldraghi/32/416_2.png) [@LionelDraghi](https://forum.ada-lang.io/u/LionelDraghi)\ **Post date:** [October 24, 2026, 8:18pm UTC](https://forum.ada-lang.io/t/spark-within-ci/4888/12 "2026-10-24T20:18:29Z")
> [@pyj](#): > > I’ved knocked out a lot of steps by allowing shortcuts via proving more in long chains, instead of relying on implicitly deduced intermediary results (adidng pre/post, or adding Assert, or Assert\_And\_Cut). In my limited experience doing this, 82k steps is more than 10x what I normally see. Yes, your’re right, a single check is donne in more than 70k steps and 20s. The second is 2k steps and the third 1,6k. It seems that CVC5 is confused on this one, Z3 is doing the job in no time. Interesting : there is the same check twice, once on the x axis and once on the y axis. Z3 uses 1 step on both, CVC5 73k steps on one, 1 on the other. The lazy solution proposed by GLM is to put Z3 before CVC5 in the list of the provers 😄 I have a better view now of what is normal and what is not, thanks.