Yeah, the interesting thing to me with formal methods is where you write some (partial) specs to tell the LLM what you want. It'll do the usual stuff, plus extra proof work to make sure your intent was actually realized.

Throwing tools haphazardly at the LLM and hoping they increase the correctness of its output is expectedly pretty ineffective. Good to see this borne out in the article.