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

Do you have any of these presentations available publicly? I'm always amused by the glitch names people come up with (force quit wrong warps, skirtless parry-walks...) and it'd be fun to see them in a TLA+ context.