IMHO Model checking is really cool. After my PhD (and reading the Baier and Katoen book) I seriously thought about getting a 'real' job in industry and applied for a job at one of the major automotive field bus software vendors. They gave me a protocol design interview question I could prepare for. So I thought: cool finally a good case to spin up a model checker (I think it was even prism). It was total puzzlement on their side when I told them how to fix the protocol bug. I think it was the time when I understood that I was unfit for many engineering job.