And just because you model the system in tla+ and its a valid model doesn't mean the vibe coded implementation matches the tla+ model