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