If you don't even check what you're formalizing you must REALLY trust the agents.

I guess if they found real verifiable bugs then it's good

We are all good as long as we are all in agreement that vibe-coded TLA+ is just a tool for the agent to do better work, not something that magically proves the code is "correct" in a useful sense