LTL with an “until” operator can specify some interesting properties https://arxiv.org/pdf/1802.06038.pdf (Definition 3.3).
Modality of the past is sometimes convenient (if player A has cheated, it can be punished). Or, in Casper contract, other branches are also important (if player A contradicts what it said on another branch).
Regarding Coq, the thrid author of the above paper is somebody to contact.
You might be interested in modeling
They define rather involved games, so a rigorous analysis is welcome. I modeled Plasma MVP a bit in Coq, but it’s currently halted.