  We present the first game characterization of contrasimilarity, the weakest
form of bisimilarity. The game is finite for finite-state processes and can
thus be used for contrasimulation equivalence checking, of which no tool has
been capable to date. A machine-checked Isabelle/HOL formalization backs our
work and enables further use of contrasimilarity in verification contexts.
