Also, I would like to know why Google didn't go for seL4 and instead created Fochsia?
I wanted to mention that we wanted to see if we can use L4 for isolating our network filter from Linux kernel (trustability) but instead we opted for bitvisor (much simpler code base but not verified).
We have a little operating system, or enough of one to facilitate building the rest of our product atop of it, that goes along with seL4. We'd planned to open source parts of it fairly soon, but prioritizing hiring a few more folks (BD, PM, Eng.) has put that effort on-hold temporarily.
Building things with seL4 is easy to do wrong, despite being given a variety of very low-level verified primitives to work with. You still need to put it all together just right. CAmkES is supposed to make this easier, but our experience with it wasn't very good, so we took the hard road and created a Rust-based application framework to go over the top of everything.
This was our main stopper. seL4 would benefit greatly to teach how everything can be fit together, and where everything can be expected to go.
Basically by providing setup, resource management, and communication abstractions that you just can't get wrong because doing something dumb that would be entirely nuts and/or would result in difficult to deal with run-time errors (as the kernel enforces some of its guarantees) ends up being rejected by the compiler ahead of time.
We have some self-driving car customers, but that's just because they're gluing together really complicated systems from lots and lots of diverse components, so they're great use cases.
Our goal is much broader scoped beyond AV and is more akin to creating new classes of CAE tools for SISoS & CPS designers/engineers.
"Can you build actual systems with it?" https://www.youtube.com/watch?v=lRndE7rSXiI&t=22m
The whole talk is well worth a watch.
I am not aware of any other capability based and verified micro kernel in level of [se]L4.
But Google may have other reasons to reinvent their kernel (though they're not starting from scratch; Zircon evolved from the Little Kernel by Travis Geiselbrecht). They may have decided that the flexibility of inventing a new microkernel for their exact requirements and moving fast with it would be more productive than reusing an existing one. Building on the careful verification process of seL4 is presumably quite time-consuming, and might get in the way.
When NeXT/Apple started using the Mach kernel, it ended up being heavily rewritten to support Apple's requirements, and they never adopted the microkernel design. Google may have seen a seL4 dependency as being a similar kind of burden.
seL4 is also GPLv2, I believe. Might also be a blocker for Google.
It will probably be like any other modern OS, but designed to be a modern OS from the beginning.
Which might save Google 0.1% in electricity costs.
Unlike the current situation with the Android ecosystem right now, where a newly released product is lucky to get even a few security updates in a year or so, and have effectively had support dropped after that.
Compare that to the ChromeOS ecosystem, where Google guarantees 5 years of support from the time the first production on a platform was released.
I don't think they only wanted to reinvent the wheel and I don't think trustability was one of the motivations of their design!
"Another fork of L4-embedded is what now runs on the Secure Enclave of all Apple iOS devices."
All Apple iOS devices is pretty big.