In this talk, we will give an overview of the additions and improvements to mCRL2 from the last couple of years. First, the mCRL2 language has been expanded with the possibility to specify probabilistic behaviour. Second, there are several new and improved implementations of behavioural relations: the GJKW algorithm for branching bisimulation with complexity O(m log n), several new preorders and an implementation of probabilistic branching bisimulation. Model checking with the modal mu-calculus has been expanded with the possibility to generate evidence in the form of a counter-example or witness. Furthermore, there are some new techniques to support model checking of infinite-state systems. Finally, there is a new, more intuitive tool for developing specifications. This tool is called mCRL2ide and it support visualisation of state spaces and also model checking of mu-calculus properties. Throughout the talk, we will do several demos.