[ajdude]

There was a pretty good article a while ago on how using verified SPARK (a subset of Ada) could help with llm generated output https://arxiv.org/html/2502.07728v1