So essentially: One cannot trust the code produced by an LLM, even if the code is a formal proof passing the verifier.

Trust in formal reasoning is necessarily always conditional. You have to start somewhere. The good thing about verified formal proofs is that the only way they can be in error is if the verifier is faulty. This drastically limits the possible reasons for error.

(In practice, there’s also the possible error that the proved formal statement means something different than what you thought it meant.)

One can only trust a verifier as far as they can trust anything made out of software.

It has nothing to do with LLMs. One cannot trust the proof of anything if one cannot trust the verifier.