In recent years, many techniques have been employed for game design. Programs have been written in various languages. Although these programs are very satisfactory in terms of accuracy of the results, speed is a factor that can definitely be worked on. In our approach to game design, we employed "Model Checking" techniques. Model Checking is the process of checking whether the given model follows certain specifications. We use the Model Checking approach to design and implement four games: "Missionaries and Cannibals Problem," "Bridge-Crossing Problem," "Theseus and the Minotaur Problem," and "Theseus and the Minotaur- Chess Style."