To support your point, Jared Davis and Magnus Myreen did the Milawa prover that builds the logic and implementation in layers starting with a hand-checked, tiny logic. Builds all the way to first-order prover with each layer getting re-checked by those below where feasible. Uses Myreen's method for verification to assembly (or machine code?). So, it's already been done.

http://www.cs.utexas.edu/users/jared/milawa/Web/

The other approach I investigated was proving the logics sound in set theory given it's well-understood, trusted, and widely deployed by mathematicians. Once the logics like FOL or HOL are verified, we just have to verify the specs and checkers (already done to in progress). Run on diverse hardware to prevent glitches there. From then on, mainly just look at logical specs since we should be good. I also found a verified compiler that uses Z specs with Prolog code... a method that might be used with Milawa for bootstrapping trust.