In a world where computers are part of our everyday life, ensuring software systems safety and correctness is crucial. To improve our trust in computer programs, a common approach is to use automated verification tools that are able to analyze a program and inform the users if safety issues, vulnerabilities, or bugs are detected. Relying on such automated tools yields an important question: who verifies these tools? In other words, who guards the guardians? This problem has been studied for more than a decade and projects such as the CompCert compiler or the Verasco static analyzer opened new routes towards the formal verification of tools dedicated to program analysis. In particular, both CompCert and Verasco have been developed within the Coq proof assistant and are shipped with complete formal proofs of their correctness. Although the formal verification of large programs requires a significant amount of work, it guarantees an incomparable level of reliability. Following this approach, we investigate the formal verification of a software model checker in Coq.