[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