Bootstrappable builds

The fabrication is shown to be correct using traceability. That is, every part of the proof is expressed in matching parts in hardware, and there is no additional hardware. This leads to a very different hardware design, one which will not perform well (eg, it's desirable to have a very long instruction word, as that makes traceability easier, but there's a high cost to fetching such instructions from memory. Especially since instruction caches and pipelines are very difficult to model, and so are usually not present).

That's the design issue for responding to Spectre. We want mathematical proof that processor designs don't leak state between processes. But we don't want to pay the price for the extreme proof and traceability of cryptographic processors.