Re: CPU
"Even if they haven't, it is one tick box off on the way to proving every component is secure, which is note- and praiseworthy surely?"
Well, it may indeed prove to be one tick box off on the way to a secure system, but in some ways it's the smallest (and therefore easiest) part to do.
Writing a compiler, run time library (nb the kernel may very well not use any library code) and designing the hardware are arguably much larger and more expensive jobs. Particularly the hardware; formally designing a fast-ish CPU is going to be $Billions.
The micro kernel is going to be only a few thousand lines of code (pure guess, but it is micro). Compilers and runtime libraries have many more lines of code than that, and they too need to be correct.
It will be interesting to see it though.
Biting the hand that feeds IT
