* A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants, https://arxiv.org/abs/2508.18587v1
* CoqPilot, a plugin for LLM-based generation of proofs, https://dl.acm.org/doi/10.1145/3691620.3695357
Before suggesting to use LLMs to completely rewrite this sort of software, there is a reason why compilers need to be certified to operate in safety critical environments. Not everything needs to use LLMs as the solution to a problem.
I would go as far to say that using an LLM in this context is the wrong solution and is irrelevant to critical systems. Maybe some here see everything as tokens and must solve everything in the form of using LLMs.
Rewriting a toy web app using LLMs from Javascript to Typescript is great, but isn't good for safety critical systems.
It's also not aviation or medical. So perhaps it's more common than you imagine.
Certainly it's not on the "AI industries" list of priorities. Perhaps, however, it's not supposed to be. I use AI tools for the use case I mentioned. The source code, build system, binary artifacts and hashes are still regulated in the way I described. The fact that the AI industry was involved in that chain simply isn't relevant.
Other uses cases involving real time agents and whatnot are another story. I'm not dealing with that problem. I suspect the AI industry doesn't really care about such attestation at this point because everyone is still in the frothy world of "new!" and the bureaucrats simply haven't caught up yet, and the adopters are taking advantage while they can. That pattern has recurred throughout the history of communication and computers.
I don't really object to that. There will be plenty of time for security theater after whatever limits are eventually found and exploited, and in the meantime there is free oxygen available.