First Advisor

Bart Massey, Ph.D.

Date of Award

Spring 6-14-2024

Document Type


Degree Name

Bachelor of Science (B.S.) in Computer Science and University Honors


Computer Science




collectible card game, formal methods, formal specification of games, Z specification language, game design, Hearthstone


Collectible card games (CCGs) have been a wildly popular game genre since the release of Wizards of the Coast’s Magic: The Gathering. These games revolve around their thousands of cards and the hundreds of thousands of interactions they can create with their many effects. For designers, it is an incredibly demanding task to ensure that every single card works properly and that each card’s text unambiguously conveys its intended behavior in all cases. The task only grows more difficult over time as the number of cards in the game grows and card effects become more complex or experimental. If the implementation and clarity check is done inadequately, it results in confusion that interferes with players’ enjoyment of the game and with designers’ development work. Players are forced to stop playing to try and resolve a conflict between card effects based on unclear texts, while designers must spend extra resources to fix the errors and clarify the ambiguities. I propose formal methods as a way to ease these challenges, help designers understand their CCG’s cards and mechanics more deeply, and facilitate the design process. I present a specification for a reduced version of Blizzard Entertainment’s Hearthstone that can be given to general theorem provers and expanded upon as a proof of concept.