I believe this, but it is also a unique case where the pitfalls of LLMs (producing weird errors that a human wouldn't) are zeroed out. Since you have a proof checker that tells you if the LLM did it right.

I'm pretty convinced most serious software will have some kind of proof system inside within the next few years.