The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine Code That Runs It).

Magnus O. Myreen, Jared Davis

Browse the full ITP paper archive.