What strategy could one use to formally model a game and prove that the rules do not lead to any self contradiction?
A major example that comes to mind is Magic the Gathering. The card interactions can get so complicated that there are several levels of judges in competition whose major role is in clarifying card interactions that come up. Now, as far as I know there has never been a situation that could not be decided (to the extent that the rules had to be altered), but how would one prove this could not occur?
A milder example is Go. This game is (I believe) fully self consistent, at least under the Chinese Scoring system. However, if you read the Wikipedia article on Go I believe the rules are underspecified in that they don't fully settle what happens when people are stubborn in territory disputes (namely how to decide if a stone is dead) after both players pass: https://en.wikipedia.org/wiki/Rules_of_go In this link user 'Andy' gives what I think is a well defined specification of the rules of Go: https://boardgamegeek.com/thread/457202/rules-about-end-game-dead-stones/page/2 In summary, what I am looking for is a general method of converting rules of popular games to a formal model which we can check is self consistent.
I ask this question here rather than card/board game Stackexchange because I think it is really a mathematical modelling question.