For verifiable domains, this really is the sweet spot.
An annoying aspect of verification-in-practice is that it is just really bulky—there's a lot to type in, and it's tedious.
LLMs, especially the latest crop of weak-reasoning models, are great for this.
Only after telling it that I tested the code and that it works did it somewhat accept that the solution worked.
I think a deterministic, unambiguous process is a lot more valuable for formal verification.
[0] https://chatgpt.com/share/67aefb63-f60c-8002-bfc6-c7c45b4520...
In my experience, if I ask it to do web things in PHP or Java, data things in Python, ... it gives a good enough result. If I ask it a postgis question, I get an answer with hallucinated APIs, bugs, and something that doesn't even do what I want if it works.
I suspect the ADA/Spark world and the formal verification world are to small to decently train the AI.
Or to phrase it another way, there must examples of the technique that you want to "generate" in the training set otherwise the horrifically overfitted model cannot work.
Probably a little bit too cynical but this is my experience asking LLMs "unusual" questions.
I tried asking a LLM for a full code snippet for the first time yesterday (i've been using them as search engines better than google, which isn't saying much, before).
It produced code that compiled but failed to do anything because the 3rd api call it generated returned an error instead of doing what the LLM said it would do.
Didn't spend time on seeing what was wrong because we already had a library that did the same thing; I was more testing what the LLM can do.