We beschrijven achtergrond, leerdoelen en opzet van een lesmodule over modelchecking voor klas 5-vwo, die dit jaar voor de derde keer verzorgd wordt in een samenwerking tussen de Radboud Universiteit Nijmegen en het Olympus College te Arnhem. Tevens doen we verslag van onze ervaringen bij het geven van deze module.