This makes sense, although it's not well described here.

Formal methods, as in proof of correctness, have been around for decades (I was doing that stuff in the 1980s) but pushing the proofs through was too laborious. The seL4 verification effort reportedly used over a decade of people time.

The idea is that if you have a formal specification of what you want to happen, you can get a LLM to do the struggling with the proof system to get it right. It's a good task for an LLM, because there's feedback from the prover.

I'd like to see more non-trivial examples of this. People keep republishing verifications of greatest common divisor or stack algorithms, which was done decades ago.