On top of what Andrew said, "failure as reachability" is a property of the implementing model checker, not the formalism itself! If you convert "we can win the game" to "it's not true that always we haven't won" and write that up as a TLA+ formula, you get `". But that means "we win in every behavior", aka `<>won`!

A really good paper on the difference between "possible" and "eventual" is '"Sometime" is sometimes "not never"': https://dl.acm.org/doi/10.1145/567446.567463