Comment by ajdude

Not just that, I've been seeing a huge effort in the Ada community to leverage LLMs to convert a lot of libraries into formally verified SPARK code. One of the biggest issues I see with vibe coded stuff is that it's difficult to review and difficult to prove that it's doing what you think it's doing, but with a strongly type language like Ada and formal verification with SPARK, LLM output is easy to read and easy to prove.