Trust “Down to the Metal”

Trusted Kernel... all the way to the metal. While building a trusted computer algebra system, the SANE version of Axiom, I've been looking at questions of trust at all levels. One of the key tenets (the de Bruijn principle) calls for a trusted kernel through which all other computations must pass. Coq, Lean, and other systems do this. They base their kernel on logic like the Calculus of Construction or something similar. Andrej Bauer has been working on a smaller kernel (a nucleus) that separates the trust from the logic. The rules for the logic can be specified as needed but checked by the nucleus code. I've been studying Field Programmable Gate Arrays (FPGA) that allow you to create your own hardware in a C-like language (Verilog). It allows you to check the chip you build all the way down to the transistor states. You can create things as complex as a whole CPU or as simple as a trusted nucleus. (youtube: Building a CPU on an FPGA). ACL2 has a history of verifying hardware logic. It appears that, assuming I can understand Bauers Andromeda system, it would be possible and not that hard to implement a trusted kernel on an FPGA the size and form factor of a USB stick. Trust "down to the metal".