[jy14898]

LLMs aren't relevant to aviation and medical devices

[naasking]

Of course they are. LLMs are routinely used to generate Lean proofs, so of course they can also be used to generate verified software. They probably aren't being used that way, yet, but they will be:

* 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

[camillomiller]

Exactly! And yet they’re touted as a catch all business case!!!