mCRL2 es un lenguaje de especificación para describir sistemas de eventos discretos concurrentes. Se acompaña de un conjunto de herramientas que facilita herramientas, técnicas y métodos para la simulación, el análisis y la visualización del comportamiento. La parte de comportamiento del lenguaje se basa en el álgebra de procesos ( Álgebra de procesos comunicantes ). La parte de datos del conjunto de herramientas se basa en tipos de datos ecuacionales abstractos ampliados con funciones de orden superior.
El conjunto de herramientas fue fundado por Jan Friso Groote y actualmente lo desarrolla el grupo de Análisis de Sistemas Formales de la Universidad Tecnológica de Eindhoven , Países Bajos .