WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+ | Publicación