With a Formalization in Isabelle
The verification in Isabelle of SimPro is described here:
Jørgen Villadsen, Anders Schlichtkrull, Andreas Halkjær From: Code Generation for a Simple First-Order Prover. Isabelle Workshop 2016: http://www21.in.tum.de/~nipkow/Isabelle2016/
Please provide feedback to Associate Professor Jørgen Villadsen, DTU Compute, Denmark: http://people.compute.dtu.dk/jovi/
Our PAAR 2018 version is here: https://bitbucket.org/isafol/isafol/src/master/Simple_Prover/
The newest version is here: https://github.com/logic-tools/simpro/blob/master/Simple_Prover.thy
Based on:
Tom Ridge: A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic. Archive of Formal Proofs, September 2004, https://www.isa-afp.org/entries/Verified-Prover.shtml (Formal Proof Development).