This project proposes to model the cooperative board game Bomb Busters using epistemic logic to capture how players reason about hidden information and coordinate under communication constraints. The aim is to develop a formal representation of game states, players’ knowledge, and uncertainty using structures such as Kripke models, and to describe gameplay actions (e.g., hints and moves) via dynamic epistemic logic to analyse how knowledge evolves over time. Specific game levels will be encoded as formal instances, enabling systematic analysis of whether winning strategies exist and how they can be derived. The project will explore automated reasoning support using MCK (Model Checking Knowledge), a tool developed at UNSW, to verify knowledge properties and synthesise or evaluate strategies; optionally, aspects of the model may also be mechanised in Isabelle/HOL for higher assurance. The expected outcome is a precise formalisation of Bomb Busters, accompanied by case studies demonstrating strategy synthesis, contributing both to the theory of epistemic reasoning in multi-agent systems and to practical insights into coordination under uncertainty, with potential relevance to distributed systems and security.