Model checking algorithms are typically complex graph algorithms, whose correctness is crucial for the usability of a model checker. However, establishing the correctness of such algorithms can be challenging and is often done manually. Mechanisation of the verification process is crucially important, because model checking algorithms are often parallelised for efficiency reasons, which makes them even more error-prone.