We present a formal proof, carried out in F*, of the soundness and the completeness of an LTL model checking algorithm based on SCC decomposition. This algorithm is a critical component in model checking, where it is used for the verification of temporal properties of systems. We begin by introducing the original formulation of the algorithm and we provide a faithful implementation in F*. We then identify the key invariants required for verification and state the essential lemmas that guide the annotation of the program, ultimately enabling a mechanized proof of both soundness and completeness within F*.