Este estudio se centra en la verificación formal de una versión paralela del algoritmo minimax utilizando el lenguaje de modelado mCRL2, aplicado al juego de Conecta 4. El objetivo de la investigación es garantizar que el algoritmo se comporte correctamente en entornos de ejecución concurrente mediante la provisión de un modelo formal y la realización de una verificación rigurosa.