When I present TLA+ [0], I am referencing game pauses (pause buffer / item duplication Legend of Zelda exploit, Dark Souls menuing to cancel animations) and deliberate crashes as mechanics to exploit games, as those are still valid actions that can be modeled, and not doing that allows such exploits to happen.

A system is only correct relative to the transition system you wrote down. If the real system admits extra transitions that you care about (pause, crash, re-entry, partial commits), and you didn't model them, then you proved correctness of the wrong system.

[0] https://lamport.azurewebsites.net/video/videos.html