Best LLMs for ADA (SPARK) - Hobbyist

Anyone has experience with LLM for Code Development? I can’t type with 10 Fingers anymore after a stroke last year and work alone on it as a Hobby. LLMs have been a Productivity Boost so I picked up coding as a Hobby again.

My goal is to put more useful ADA and ADA SPARK libraries on public into Github. So LLMs can eventually one-Shot ADA (SPARK) Code for different tasks (LLMs are Marketed as „they can do anything? - well that would be a real gain of function).

My experience so far;

  • ChatGPT Pro (used till 02.2026) - Produces unusable Code, unable to provide fix
  • Gemini Pro - recently got quite good in ADA, but copypasting answers is tiresome
  • Mistral Code - is ok for ADA, I Like that it does directly edits Github Repos. But it ate 50%+ of my Usage Limit on a Single task and now it’s done for the month.

I don’t want to spend more than 20 € a month on this, since it’s just a Hobby.

My Workflow is usually I Update Main Branch in Github, Download and Extract, then run GNATPROVE, gnatmake or a Makefile from the Terminal in the Folder.

I have turned to writing ADA versus ADA SPARK, since I prefer Instant Compiler Feedback to 15+ Minutes waiting for GNATPROVE.

My assumption is the more useful ADA Code there is out on Github the faster LLMs will become at writing it.

Any ideas where to best invest my time/Money in this? Maybe there are ways I can Automate the Verification with gnatmake / gnatprove (me having to do this locally seems the biggest bottleneck right now).

Thanks for Reading and your Kind attention to the matter.

Robert

I haven’t done much with it, but for the little I have done, Copilot did okay. It forgot a couple of with statements, and I vaguely recall that there were a couple of other issues, but they were all easily fixed.

That said, the problem I threw at it was relatively simple: implement a statistical method in Ada code, because I didn’t want to use Excel and I didn’t want to spend 1 week debugging my own hand-written Ada code. YMMV

Gemini is … ok. Grok build is much better than you’d expect. It has one shot multiple programs for me.

Copy/paste the proofs to the AI and have it have a look. Supposedly AdaCore is making skills available for this (@markhermeling).

Tune your command line for faster turnaround. My command takes isn’t instant, but it’s not multiple minutes.

alr gnatprove -j12 --level=2 --steps=20000 --counterexamples=on

Add --report=statistics to show which proofs take the longest, and you can optimize those.

Fantastic idea! Here are some of my thoughts:

I find the $20 Anthropic subscription worth it. That is what I use for my personal projects. I have been using HuggingFace as well and I know people are using ollama.com.

The frontier models do fantastically well, though my benchmarks are small problems (see github.com/AdaCore/ada_eval). In the open sence, GLM 5.2 and DeepSeek V4 and Kimi K3 do best. Nemotron is not bad, but a bit lower at the moment.

Best results in the open models is if you guide them closely and provide an ‘oracle’, a way to measure good. In my cases, the oracle is 1) build; 2) no formatting warnings; 3) SPARK Silver and 4) test passes. This is provided as a single command for the agent to do after every step.

I believe SPARK makes a difference as the agent can see what is good, yes, compile/prove is a bit longer, but as @pyj mentioned, you can tune your command line.

I still need to write this up in a blog post, but it is a side-project for me right now and I can’t spend a ton of time on it.

Join us in the Office Hours on Fridays at 10am ET if that is possible in your timezone and we can chat more.

Thanks for all your quick responses! I will Explorer the options and have a look. I was thinking Grok might be good at it, since SpaceX probably used ADA for their Rockets/satellites, at least in Part.

Gemini has just gotten way better with that task. In 12.25 it took like 4 Hours and 25 iterations Till I had working Code (that was ADA SPARK on GNATPROVE Lvl 4 though).

I think it’s probably due to trying GNATPROVE Lvl 4 that local testing takes so long.

But current Project anyway is to generate Algorithms in ADA + Tests from this Wikipageand put those up as public Repos on Github. After that can look at Algorithms that are beneficial to Implement in ADA SPARK as well.