Apalache is a symbolic model checker for TLA+ that translates specifications into logical...