A Fully Verified Executable LTL Model Checker by Javier Esparza π, Peter Lammich π, RenΓ© Neumann π§, Tobias Nipkow π, Alexander Schimpf π§ and Jan-Georg Smaus π May 28