Please excuse my ignorance. I'm an 'old-fashioned' guy who thinks that there is just 'software' and 'hardware' - and these are two separate things. Along this line of thinking an OS is part of the software, and a microkernel is part of the OS. (I'm aware of the debate about Microkernels - and how Linux didn't really end up using one).
So when I hear the quote:
I'm aware that L4 is the microkernel that has been 'proven correct' against its specification. But to me - that is part of the OS. (ie loaded from disk into memory and then instructions are transferred down to the CPU over the Bus.)
My question is: How does part of a microprocessor (Apple secure enclave) use a microkernel (L4)? (Is this a kind of FPGA? Do they feed it into the part that lays out the transistors and 'embed' the software in silicon?)