For context, the Apple Secure Enclave chips run an NICTA L4-based microkernel, albeit not SeL4 specifically as far as I know (given the Secure Enclave launched in 2006 and NICTA released SeL4 in 2014). I wonder if this indicates plans to adopt SeL4?<p>SeL4 is extremely cool technology. It has been formally proven to be bug-free against its specification, which massively simplifies the development of high-security high-reliability systems. I feel like there’s a lot more development to be seen in this space.
If you're interested, the microkernel is open source: <a href="https://github.com/seL4/seL4">https://github.com/seL4/seL4</a>
A little bit unrelated, but reading through their member list:<p><a href="https://sel4.systems/Foundation/Membership/" rel="nofollow">https://sel4.systems/Foundation/Membership/</a><p>reminds me that Jobs explains why their company called "Apple Computer" is: "I worked at Atari, and it got us ahead of Atari in the phone book."[1].<p>Apple is the first one of all sel4 general member too.<p>[1] <a href="https://www.businessinsider.com/apple-archive-name-apple-2011-12" rel="nofollow">https://www.businessinsider.com/apple-archive-name-apple-201...</a>
Hopefully they won’t be the absolute waste of time as a company that they have been on the web standards working groups. Hard to trust them at this point in any collaborative sense.
Interesting if unsurprising this is shortly after the AArch64 verification was completed.<p>And credit where it’s due, I know we love dumping on the national security apparatus, but the UK NCSC actually funded that work, which is a clear net win.