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.
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
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.
Personally I am mostly chilling with Opencode’s free tier (Zen) where there are no API keys required at all. Otherwise OpenRouter and Omniroute are good alternatives to look into.
Model wise I am finding good results with Deepseek V4 Flash Free, though other decent models include Laguna, Ling and Hy3. Did not really bother going for a subscription as they tend to be somewhat pricey. Wish I could get Gemini/AI Studio to work but the site itself has been finicky to deal with,
I personally use OpenCode Go (10$/month) and I also mostly use DeepSeek v4 Flash. It is so cheap I barely use the full subscription and when I do I default back to the Free tier of Zen or Nemotron. I also use the free models in OpenRouter, you only need to have some money deposited in it to have the quotas raised by a bit. They do this to prevent purely free leeching.
I want to try out Laguna and Hy as they seem to be widely used too.
If you go into my profile, you can read some (slightly outdated) posts about my experience using AI which has been mostly positive and improving.
No matter the model one uses, using plan mode at the start of a session before switching to build always seems to yield infinitely better results for complex use cases.
I’ve had luck with both the Codex and Claude tools. They leapfrog each other in terms of how well they do, but I’ve been particularly impressed with the Anthropic Opus model lately w/ SPARK.
Little feedback; I have been using my existing subscriptions and spare time to generate more algorithms + V&V Test suites in Ada as GIthub Repos. My summary;
Mistral Work does ok if it gets it right first second or third time, but after that it can get caught in its own edit mistakes and then starts simplyfying too many things.
Gemini on Plus subscription with Pro and Extended mode on manages to one-shot 1/8 or takes 1-3 edits.
Even Gemini Flash-Lite Extended does well
So for now I go with these till the list is full. Then I test how the models do on Algorithms in Ada SPARK. But thats still like 850 or so algorithms away.
Thanks again everyone for your feedback, appreciate it.
Bit unrelated but I feel this might be a useful AI skill to use especially with the more technical projects.
It makes docs output conform to ASD-STE100 Simplified Technical which avoids the flowery language base LLMs like to output.
Disclaimer: I am not the author of this, just a happy user who found out about it recently. So far it is quite nice for docs in one of my Ada projects.
As I am mainly using only free providers (avoiding vendor lock in, API key and account hassle among other reasons), my current setup is freebuff (1 hour free of GLM 5.2, 1 hour of deepseek v4 flash free 07 31 if off peak or a similar model), kilo’s and opencode’s free models (opencode model limits reset daily, kilo’s is hourly. Do note certain free models use your input and prompts for model training (deepseek v4 flash free, muse spark contributor). It is fine for my use case of mainly open source projects on GitHub (which Microsoft scrapes anyway), though one should look into this caveat with free models for more mission critical or sensitive use cases.
I would like to update my perspective on AI after some further testing and tackling harder problems and larger refactors:
TL;DR: I am now burning more money as cheaper models are no longer that cheaper and the tasks I am now doing are more complex, which simpler models cannot handle.
Something interesting is cost. GLM is very very very expensive when compared to the cheaper models. Though itself is also cheaper than frontier ones. Nevertheless, I have seen my cost go waaaay up, specially since DeepSeek increased its prices a couple of weeks ago. As the cheaper models I used to use are no longer extremely cheap, I have started using more expensive models such as GLM.
More advanced models with Ada perform much better. However, as I said, they cost way more than cheap ones. This creates an interesting tradeoff… Do I want an expensive model that will correctly do the task or a cheaper model that will take longer and probably need a large amount of inputs and refactors?
The outcome of expensive models is that I BURN cash, but not only because of their increased price. I find myself finishing tasks much faster and better, so I want to move even faster (mainly because I can focus on features rather than guidance or fixes), which increases the burn rate. Cheaper models take longer to complete a task, so they also burn a bit of money even if they cost less. However, in terms of cost-vs-completed-features, Cheaper models are still very useful for simpler tasks (specially when they are good at it).
The simpler models are no longer cutting it that well. I started doing larger refactors of my project, specially SPARK related ones, and the smaller models could only do the basic tasks. The harder problems have required GLM-5.2 (5.3 should be open, but the weights are still not there) or DeepSeek v4 Pro (the latest weights), but GLM-5 is preferred.
This is in line with Mark’s findings during his testing. You can find his work and experience in the past few SPARK office hours.
(DISCLAIMER: I have not used closed-weights models, so no ChatGPT nor Claude.) From what I have seen other people do with the US frontier models, they seem to be cheaper than the expensive open source ones… How can that be if they are usually 2-5x more expensive? I have seen that frontier models are much better at succeeding at a task faster, so they “think” less and finish faster, so even if they cost more, the final price is not that high. They have also been reported as being more token efficient. I cannot contrast this information, but that would also align with what I am seeing. It is also the case that US models are being financed (read, run at a loss) while open weigh models are run by several parties and while some may be willing to take a loss, most don’t, so their prices are more realistic.
Hello everyone,
Following the fascinating discussion here on leveraging LLMs for Ada/SPARK development, I would like to share a different perspective—and a concrete technical contribution—regarding how we bridge the gap between probabilistic AI and critical software engineering.
Treating RLHF (Reinforcement Learning from Human Feedback) as a reliable safety mechanism is often a illusion; it acts merely as a cosmetic patch on statistical weights, introducing internal conflicts, smoothing out stochastic extremes, and creating statistical inertia.
To truly make LLMs useful and safe—especially for hobbyists or safety-critical applications—we shouldn’t just rely on prompt engineering or manual copypasting. We need mathematical confinement.
I have recently published open-source Ada/SPARK frameworks tackling this exact problem (available on Zenodo and GitHub under the LPV3 license):
V3 LLMS Deterministic Guardrail & Execution Supervisor (v3_llms_guardrail_supervisor.adb):
A critical deterministic supervision system complying with DO-178C DAL A standards.
Enforces strict safety rules (immediate flow cut and maximum confinement if guardrails breach or human interrupts occur, and memory sanitization for recursive loops or hallucination spikes).
Uses bounded types, saturating arithmetic (zero overflows, zero divisions by zero), and modulo-9 digital root checksums verified statically via SPARK.
RLHF Instability Simulation (rlhf_instability_simulation.ads):
A formal simulation model exposing how RLHF creates internal incoherence, prevents proper self-verification, and rejects novelty.
By moving the safety burden from runtime guesswork to SPARK’s formal proof engine, we can mathematically guarantee termination, lack of overflow, and structural integrity without waiting 15 minutes for proofs, provided we structure our types and contracts cleanly.
Happy to chat more about how formal methods can tame probabilistic models!
Best regards,
Dr. Benhadid Outail (ORCID: 0009-0003-3057-9543)
“To truly make LLMs useful and safe—especially for hobbyists or safety-critical applications—we shouldn’t just rely on prompt engineering or manual copypasting. We need mathematical confinement.”
How is what you have mentioned not prompt engineering, unless I am missing some way your “framework” actually forces the LLM to comply in some way. If you are not using standard skills or MCP to tell the LLM to comply I am not sure how you are going about it.
“Enforces strict safety rules (immediate flow cut and maximum confinement if guardrails breach or human interrupts occur, and memory sanitization for recursive loops or hallucination spikes).
Uses bounded types, saturating arithmetic (zero overflows, zero divisions by zero), and modulo-9 digital root checksums verified statically via SPARK.”
I am curious how your framework enforces this.
“By moving the safety burden from runtime guesswork to SPARK’s formal proof engine, we can mathematically guarantee termination, lack of overflow, and structural integrity without waiting 15 minutes for proofs, provided we structure our types and contracts cleanly.”
Is that not the whole point of plain old gnatprove? Also there is a flag which lets you use more CPU cores with gnatprove and you can always implement some sort of caching mechanism on top of it.
I must have missed quite a few points while reading this. Also it would be helpful if you could link the projects here.
At the end of the day though, I do agree on the need to tap into deterministic tooling that does not lie.
P.S. After reading through again, your work is definitely great and great for mission critical use cases.
“TL;DR: I am now burning more money as cheaper models are no longer that cheaper and the tasks I am now doing are more complex, which simpler models cannot handle.”
Yeah when using free or cheaper model providers we are pretty much at the mercy of their price changes at any given time. The few remaining truly reliable and free providers for decent enough open weight models are heavily dwindling as we speak. There are some who will basically use the free tier so much to the point where the upstream infra is hammered and they have to do the necessary evil to maintain service quality for remaining users.
Which is also why I am quite wary of self imposed vendor lock-in especially with free providers, they come and go quite quickly.
From my usage with cheaper models you have to be very specific and clearly scope the set of changes you want to make. Because they are not as good as the frontier models at “inference” or “filling in the blanks” (basically next token prediction to the point where it can have a good approximation of your intention without you directly spelling it out).
Cheaper models are not the best at large refactors as you note, though I have good result with them doing medium sized ones given the right prompts even without invoking plan mode first. There is that convenience you get with frontier models I would suppose. One analogy I could give is that cheaper models feel like a grass cutter (you have to be precise in what you want) whereas the more premium ones feel like a lawn mover (you can be a bit more ambiguous in your input and with more of certain types of training data the model is able to better guess what you want).
Their “behavioural differences” boil down to the sources, types and amounts of training data used (plenty of which is copyrighted and most probably obtained under legally dubious circumstances at best).
On the legal side of things, I guess that is why the creatives (arts, writing, media etc) are not too happy. Certain influential open source projects like Zig and Codeberg are also coming out and banning AI generated contributions (for Zig) and code (for Codeberg), though their reasons are different (the AI slop fest when the hype train was taking off, and LLM scrapers cooking Codeberg infra).
Old DeepSeek V4 Pro is allegedly worse than DeepSeek V4 Flash Free (07-31 or 08-13 versions), though I have not used DeepSeek Pro myself.
Thank you for your insightful contribution on deterministic AI safety. Your V3 LLMS guardrail supervisor and formal verification approach are exactly what’s needed for critical systems.
You may find my Ada algorithm implementations on GitHub (RobertBoettcherSF) of interest—most were generated with Gemini Pro on Extended Reasoning. Once all algorithms from the Wikipedia list are implemented in Ada, I’ll commence the SPARK implementations.
Your emphasis on mathematical confinement over RLHF is particularly valuable, and I look forward to exploring potential synergies between our work.
which has been mostly positive and improving.