What you can't close is the language that you use to do all the verification in, itself. You wind up with a core calculus that you have to stare at really hard and trust / prove via other means.
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.
It's always possible there is a loop somewhere. The best you can hope for is make it infinitesimally small.
That's not to say there's no way to close the loop here, simply that I don't know that this is it.
A medium-assurance solution is 3+ compilers with same input and output on diverse hardware by diverse teams unlikely to collude all producing ssme result. If hardware, you can do that with chips plus voting scheme.
EDIT: Whew!
http://www.cse.chalmers.se/~myreen/
Follow he and his colleagues work for all that. Especially Milawa and CakeML. If you want a starting point, a small, Forth-like processor verifiable by hand on a node verifiable by eye could run the initial interpreter and prover for the first, real CPU. Plus, common practice is to split work into untrusted generation of artifacts with traces that are verified by a trusted checker that's comparatively tiny and simple. The little CPU would just run the checkers. You can run the generation on anything you like with the speed benefit. :)
As far as I understand modern truly reliable system (commerical avionics-like) still must be relatively simple to be verified up to hardware level.
http://www.spbguga.ru/files/Formal_Verification_of_a_Process...
http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf
VAMP is a pretty-complex, DLX-style CPU. I think they extended it to multicore or concurrency of some kind in another work. Original was single core, though. Passed all the FPGA tests. The AAMP7G combines a stack machine, over a hundred instructions, microcode engine, and separation kernel into one CPU. It was first in recent times in high-assurance security to use microcoding. I tell everyone to do that since it lets us easily change the behavior of the hardware without reverifying everything. Their tools also let you verify software semi-automatically against a model of the hardware ISA. Main stuff is paywalled but this is best free one I could get you. On availability side, they also run three units at once with a voter to reduce the odds the chip will fail. Truly high-assurance exemplar in availability and security.
The prover is ACL2. You can do a trusted checker for that in few lines of code. You might need a lot of RAM and CPU time, though. Even all that can be a few blocks verified by eye and hand that you just plaster over a bunch of silicon then verify correctness automatically. There's also techniques where a partial failure can be magnified into total, visible failure. Tandem/HP NonStop does stuff like that to catch and replace failed components before system downtime happens. So, you can be reasonably sure the components are working even if defects happen during fabrication.
[1] https://www.sosy-lab.org/~dbeyer/verification-witnesses/
Here's the one I was referencing with the tiny TCB:
https://www.cs.princeton.edu/~appel/papers/flit.pdf
OK. So, it was a few Kloc. Still smaller than Coq. They could probably get it even smaller with recent work given translation validation knocks compilers out of TCB. So, in between 803-2668loc.
https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides....
[Fixpoint terms are also CIC programs, so there's a sense in which they're related, but it's not really about Curry-Howard.]