# Lifting your project to SPARK

**URL:** https://forum.ada-lang.io/t/lifting-your-project-to-spark/4587
**Category:** General
**Tags:** spark
**Created:** [July 23, 2026, 12:58pm UTC](https://forum.ada-lang.io/t/lifting-your-project-to-spark/4587 "2026-07-23T12:58:51Z")
**Posts on this page:** 2
**Page:** 1

<div class="post-metadata">

### Author: ![markhermeling](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/markhermeling/32/855_2.png) [@markhermeling](https://forum.ada-lang.io/u/markhermeling)
#### Post date: [July 23, 2026, 12:58pm UTC](https://forum.ada-lang.io/t/lifting-your-project-to-spark/4587/1 "2026-07-23T12:58:52Z")

</div>

I have a rather sizeable subscription to some of the frontier LLM offerings. Some weeks I don’t get to using all of my allotted compute that is in that subscription, some of my weeks are simply more powerpoint poisoning rather than code-heavy.

Hence I am offering to use my leftover budget to lift projects to SPARK, if there is interest in the community. No guarantees of course, I have been sampling a few repos, some are easier than others, found a couple of simple errors, mostly off-by-one errors.

Interested? Post a link to a GitHub or GitLab repo as a comment to this post, I’ll clone it and kick off my LLM with the /gnatprove skill and send you back a PR/MR with the changes and a document that explains the reasoning of the LLM.

---

<div class="post-metadata">

### Author: ![ThyMYthOS](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/thymythos/32/870_2.png) [@ThyMYthOS](https://forum.ada-lang.io/u/ThyMYthOS)
#### Post date: [July 23, 2026, 8:19pm UTC](https://forum.ada-lang.io/t/lifting-your-project-to-spark/4587/2 "2026-07-23T20:19:13Z")

</div>

Actually I think the GNAT math could benefit from some stronger post conditions.  
For example:

- That `Sqrt (x)` is monotonic for `x >= 0`
- `Sin (x)` is monotonic for `-Pi / 2 <= x <= Pi / 2`

Right now only the trivial edge cases are stated.