MaskCharade is a Coq formalization in modal logic \(S5^n\) for the 2nd edition of Bruno Faidutti’s Mascarade board game. It is a small project for a peer-to-peer seminar at the University of Bologna as part of Eugenio Orlandelli’s Logical Methods for Philosophy course. The resulting slides are available here.