A long-standing problem in the mCRL2 toolset was the poor support for generating counterexamples of model checking properties. Over the course of the last year an effort has been made to finally tackle this problem. It is now possible to generate counterexamples and translate them back to the original model. The first applications of this new technique look very promising. In this talk I will roughly explain how the generation of counterexamples works, and give some examples. I will also explain my thoughts about how to implement such an algorithm.