This paper takes you behind the scenes of the Model Checking Contest (MCC), an annual competition focusing on the behavioral analysis of asynchronous systems using state-space exploration and model checking techniques. The MCC is part of a thriving …