# Is SPARK in ADA a theorem prover?
**URL:** https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995
**Category:** General
**Tags:** spark, ada
**Created:** [November 28, 2025, 9:01pm UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995 "2025-11-28T21:01:38Z")
**Posts on this page:** 13
**Page:** 1
### Author:  [@ValorZard](https://forum.ada-lang.io/u/ValorZard)
#### Post date: [November 28, 2025, 9:01pm UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/1 "2025-11-28T21:01:38Z")
This might be a dumb question, but is spark in ada similar to Z3 or lean 4? As in, can it be used to formally prove stuff like theorems or whatever?
---
### Author:  [@Heziode](https://forum.ada-lang.io/u/Heziode)
#### Post date: [November 28, 2025, 9:13pm UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/2 "2025-11-28T21:13:38Z")
Hi,
Someone with more expérience in SPARK will give you an answer.
But, gnatprove that prove your SPARK code, uses z3, in addition with other tools : [7.1. How to Run GNATprove — SPARK User's Guide 27.0w](https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_run_gnatprove.html#running-gnatprove-from-the-command-line)
---
### Author:  [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [November 28, 2025, 9:50pm UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/3 "2025-11-28T21:50:23Z")
SPARK isn’t a theorem prover, rather it’s a programming language derived from Ada plus static analysis tools that allows you to prove things about programs such as absence of run-time errors and functional correctness. So you write SPARK code which can be compiled with a compiler such as GNAT, then use the GNATprove tool to perform static analysis on the code which will try to automatically prove various properties on the code.
Behind the scenes, GNATprove uses Why3 and automatic theorem provers like Z3, CVC5, Alt-Ergo, and COLIBRI to prove various checks on the code. For example, given the following function in SPARK:
```ada
function Increment (X : Integer) return Integer is (X + 1)
with Pre => X < Integer'Last,
Post => Increment'Result = X + 1;
```
GNATprove will emit a verification condition (VC) for the addition `X + 1` to try to prove that the result of the addition fits within the bounds of type `Integer`, assuming that `X < Integer'Last` from the precondition. Another VC will also be emitted for the postcondition to try and prove that the returned value is equal to `X + 1`.
So SPARK isn’t used to prove mathematical theorems, but rather proves various properties about the program such as absence of run-time errors (no arithmetic overflows, buffer overflows, division by zero, etc) as well as functional properties expressed in contracts (preconditions, postconditions, invariants, predicates, etc).
That’s a brief overview which I hope answers your question. If you want to learn more I recommend checking out AdaCore’s Learn website. This page provides a nice overview of SPARK: [SPARK Overview - learn.adacore.com](https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html)
---
### Author:  [@ValorZard](https://forum.ada-lang.io/u/ValorZard)
#### Post date: [November 28, 2025, 9:51pm UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/4 "2025-11-28T21:51:20Z")
Hm, then I guess a follow question is, is there a way to do theorem proofs in Ada? Like a library for it or something?
---
### Author:  [@AJ-Ianozi](https://forum.ada-lang.io/u/AJ-Ianozi)
#### Post date: [November 29, 2025, 1:29am UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/5 "2025-11-29T01:29:51Z")
This isn’t specifically what you’re looking for, but you can prove algorithms with SPARK:
> **[I can’t believe that I can prove that it can sort](https://www.adacore.com/blog/i-cant-believe-that-i-can-prove-that-it-can-sort)**
>
> When an enthusiastic Ada programmer and a SPARK expert pair up to prove the most "stupid" sorting algorithm, lessons are learned! Join us in this…
I’m also aware of some crypto with his stuff written in SPARK, which result in them being provable (it’s no longer maintained though)
> **[GitHub - Componolit/libsparkcrypto: A cryptographic library in SPARK 2014](https://github.com/Componolit/libsparkcrypto)**
>
> A cryptographic library in SPARK 2014
---
### Author:  [@ValorZard](https://forum.ada-lang.io/u/ValorZard)
#### Post date: [November 29, 2025, 6:51am UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/6 "2025-11-29T06:51:38Z")
This article is pretty close to what I was originally imagining SPARK to be:
> **[Solving Sudoku with AdaSAT](https://www.adacore.com/blog/solving-sudoku-with-adasat)**
>
> Originally, constraint solving in Libadalang was handled by several ad-hoc solvers built specifically for different parts of the type system. These…
Seems like AdaCore already has a library that can do proof solver stuff?
---
### Author:  [@Irvise](https://forum.ada-lang.io/u/Irvise)
#### Post date: [November 29, 2025, 7:45am UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/7 "2025-11-29T07:45:35Z")
AdaSAT is open and used in production: [GitHub - AdaCore/AdaSAT](https://github.com/AdaCore/adasat)
There are libraries that already have structures fully proven that you can build on them and create more complex proofs, the main one being SPARKlib: [GitHub - AdaCore/SPARKlib](https://github.com/AdaCore/SPARKlib)
SPARK is more about proving code than rather proving the problem behind it. So in a way, SPARK is not like Rocq/Coq or Lean4, but it uses the same underlying principles and tools. If you want Satisfiability Theory (SAT) those systems may be better (you can check out SMT-Lib too) [SMT-LIB The Satisfiability Modulo Theories Library](https://smt-lib.org/index.shtml) or Operational Research tools such as HiGHS.
Best regards,
Fer
EDIT: I incorrectly stated that AdaSAT was a Proof-of-Concept when in reality it is used in production as corrected by Fabien.
---
### Author:  [@ValorZard](https://forum.ada-lang.io/u/ValorZard)
#### Post date: [November 29, 2025, 9:44pm UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/8 "2025-11-29T21:44:12Z")
For context, what I’m trying to do is create a “proof solver” for Tetris.
Think something like stackrabbit for chess, but for Tetris instead.
So, given a Tetris board, is it solvable, or has it reached a fail state?
So, I would like to be able to “prove” that certain states are valid and other states aren’t. Tbh, this feels like something more suited to Haskell, but I want to have a graphical display/simulation written in Raylib or SDL, and Haskell isn’t great for actual gameplay code from what I’ve seen.
---
### Author:  [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [November 30, 2025, 9:41am UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/9 "2025-11-30T09:41:01Z")
That sounds doable in SPARK, and you might fight this blog post interesting which implements Tetris in SPARK on an Arm Cortex-M4: [https://www.adacore.com/blog/tetris-in-spark-on-arm-cortex-m4](https://www.adacore.com/blog/tetris-in-spark-on-arm-cortex-m4)
---
### Author:  [@Fabien.C](https://forum.ada-lang.io/u/Fabien.C)
#### Post date: [December 1, 2025, 9:16am UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/10 "2025-12-01T09:16:17Z")
> [@Irvise](#):
>
> AdaSAT is open but it was just a proof of concept: [GitHub - AdaCore/AdaSAT](https://github.com/AdaCore/adasat)
AdaSAT is used in production by langkit\_support and all the libraries and tools that depend on it (Libadalang, VS Code pluging, GNAT Studio, GNATformat, GNATdoc, etc.).
See here: [Solving Sudoku with AdaSAT | AdaCore](https://www.adacore.com/blog/solving-sudoku-with-adasat)
---
### Author:  [@duggan9265](https://forum.ada-lang.io/u/duggan9265)
#### Post date: [December 1, 2025, 10:00am UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/11 "2025-12-01T10:00:23Z")
You could look into Coq which is a theorem prover written Galilea I think the language is called. There is also another theorem solver called Isabelle.
---
### Author:  [@F-Loyer](https://forum.ada-lang.io/u/F-Loyer)
#### Post date: [December 1, 2025, 10:15pm UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/12 "2025-12-01T22:15:15Z")
Coq is not written in Gallinea…
OCaml is the implementation language of the Coq tool, and Gallina is the language you use within Coq to encode and verify properties. Gallina serves as the core language for the logical framework Coq operates on.
---
### Author:  [@duggan9265](https://forum.ada-lang.io/u/duggan9265)
#### Post date: [December 2, 2025, 8:09am UTC](https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995/13 "2025-12-02T08:09:16Z")
I see, I stand corrected!