I'd guess the best approach is similar to security - minimal TCB (trusted computing base) that you can verify by hand, and then construct your proof checker on

I'd guess the best approach is similar to security - minimal TCB (trusted computing base) that you can verify by hand, and then construct your proof checker on top, and have it verify itself. Proof and type checkers have a lot of overlap, so you can gain coverage via the language types. I can't recall exactly, but I think CakeML (https://cakeml.org/jfp14.pdf https://cakeml.org/jfp14.pdf) had a precursor lisp prover, written in a verified lisp, so would be amenable to this approach. EDIT: think it was this one https://www.schemeworkshop.org/2016/verified-lisp-2016-scheme-workshop.pdf https://www.schemeworkshop.org/2016/verified-lisp-2016-schem...