There is a verified DRAT-trim (the proof checking format used) implementation in Isabelle/HOL [1]. Apparently it is faster than the original: ``We have present

There is a verified DRAT-trim (the proof checking format used) implementation in Isabelle/HOL [1]. Apparently it is faster than the original: ``We have presented a formally verified tool chain to check DRAT unsatisfiability certificates. In single-threaded mode, our approach is more than two times faster than the (unverified) standard tool drat-trim, on a benchmark suite taken from the 2016 SAT competition.'' [1] Lammich, Peter. "Efficient verified (UN) SAT certificate checking." International Conference on Automated Deduction. Springer, Cham, 2017.