Lifting your project to SPARK

General
1

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.

2

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.