seL4 actually has an end-to-end proof, which proves that the final compiled binary matches up with the formal specification. There are not many places that bugs can be shifted---probably the largest one at this point is the CPU itself.

See here[0] one of Gernot Heiser's comments (part of the seL4 foundation) talking about how "there are seL4-based devices in regular use in several defence forces. And it's being built in to various products, including civilian, eg critical infrastructure protection".

There is also an interesting case study[1][2] where seL4 was shown to prevent malicious access to a drone. Using seL4 doesn't necessarily make an entire system safe but for high security applications you have to build from the ground up and having a formally proven kernel is the first step in doing that.

I have been fortunate enough to play a small role in developing some stuff to be used with seL4 and it's obvious that the team are passionate about what they've got and I wish them the best of luck

0 - https://news.ycombinator.com/item?id=25552222 1 - https://www.youtube.com/watch?v=TH0tDGk19_c 2 - http://loonwerks.com/publications/pdf/Steal-This-Drone-READM...

>(Eh, ) I highly doubt that it will ever have a practical use beyond teaching kids in the classroom that formal verification is fun, and maybe nerd-sniping some defense weirdos to win some obscene DOD contracts.

Uh, perhaps take a look at the seL4 foundation's members[0], who are using it in the wild in very serious scenarios.

You can learn more about them as well as ongoing development work in seL4 Summit[1].

0. https://sel4.systems/Foundation/Membership/home.pml

1. https://sel4.systems/Foundation/Summit/home.pml