[tombert]

I haven’t fully given up on the hope that a fully verified kernel eventually catches on. It would be basically impossible to verify all of Linux at this point, but I could see seL4 eventually getting traction in something like the smartphone market.

A guy can dream, at least.

[meling]

It has been used for a while in the Secure Enclave operating system: https://en.wikipedia.org/wiki/L4_microkernel_family#:~:text=...

But to my knowledge, not for the more general user facing OSes.

[tombert]

Yeah that's what I was getting at. I know seL4 is used in a bunch of places, but outside of a few hobbyist projects I have never heard of anyone using is at a "full" OS.

It would be nearly impossible to have the support for the extremely diverse set of hardware that desktop Linux has while staying formally verified, but for something a bit more constrained like a smartphone, I think something like seL4 could work as a base and the manufacturer could write their own drivers for whatever hardware is needed.

I mean, how cool would it be if every single part of the stack that is even possible to verify was fully verified. I know about the halting problem, I know there are things that would be basically impossible to verify fully, but I still think it would be cool to live in a world where software engineers actually had a little assurance what they were doing actually worked before unleashing into the world.

[AlotOfReading]

I know at least one autonomous vehicle company is using it as their base OS in the autonomy stack, with efforts at extending some form of verification up to the high level code.

[tombert]

That's cool as hell! I didn't know that but it makes me happy to see it getting a bit more love.

[snvzz]

seL4 is being used in many places that we know about[0] and then there's those we don't or are still in the future, where we can only guess based on e.g. seL4 membership[1].

0. https://sel4.systems/use.html

1. https://sel4.systems/Foundation/Membership/