We're using seL4 as the basis for one of our products which is focused on characterizing components, systems, and their failure modes. Mostly targeting critical "Cyber-Phyiscal Systems" and "Software-Intensive Systems of Systems".

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.

> seL4 is easy to do wrong

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.

We overcame this with a significant amount of Rust-i-ness and effort in understanding the guts of the kernel and how it implements its assurances.

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.

What sort of mistakes were easy to make?

Was this work a part of the post's unnamed self-driving car company project?

Nope. Entirely different. Left prior place just over a year ago. Eventually started a new company and closed our Seed funding a few months ago.

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.

> This is a great view on history of seL4. Is there a list of use cases where seL4 is being used outside academia?

"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 forgot to mention that I had seen these, but I thought after so many years from L4's release something like isolating firmwares from the OS in our smartphones would have been done.

I am not aware of any other capability based and verified micro kernel in level of [se]L4.

Zircon, the Fuchsia kernel, is much bigger than seL4. For example, it provides a process model and syscall interface.

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.

because that would bore the people who are in the fuchsia team purely to not be bored?

Man, this meme that Fuschia is literally a "dont quit please, bored developers" project is huge on HN. It's repeated often like it's common knowledge. Is there any real corroboration for it, or is it just a fun pet theory people like?

The fact that Fuschia is a large project without any public purpose, roadmap, architecture process, or governance invites these theories. If you want to be so mysterious you can't complain when people speculate.

I strongly suspect that any roadmap would mostly consist of features present in other existing OSes, removing the mystique.

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.

*Fuchsia

From what I've seen, I believe that Fuchsia is intended to eventually replace GNU Linux based Android as the mobile platform for Google... eventually. The idea is to have a good platform for VR/AR apps (soft real-time processing / rendering), while providing a system that can be continually upgraded.

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.

Bored?

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!

TFA mentions:

"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.

But L4-embedded is not seL4. It would be cool to see some large-scale deployment of a formally verified system.

FWIW, OK Labs was acquired by General Dynamics in 2012.