[alexisread]

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) 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-schem...

[guerrilla]

This is correct. That's why you have core type theories. Very small, easy to understand and implement in a canonocal way. Other languages can be compiled to them.