It seems that you are looking for the supplemental material of the paper “A Fully Verified Executable LTL Model Checker”. We moved it to the Archive of Formal Proofs for long-term archival and continued maintenance.