Courses on formal methods are often based on examples and case studies, supposed to show students how to apply formal methods in practice. However, examples often fall into one of two categories: First, many are artificial and thus do not relate to practice. Second, examples are based on projects of industry partners and are, thus, way too involved for students to understand them. In this paper, we present a different approach. By formalizing the rules of commonly known games, we achieve examples both engaging and suited for students. Furthermore, we broaden the horizon of formal methods, driving research at the same time: we present extensions such as playable visualizations and explore the relationship between game AIs and model checking heuristics.