I formally modeled Dreidel for no good reason

It uses PRISM, a "probabilistic model checker", so not your typical theorem prover or SAT solver.