seL4 is far more rigorous that the others. The problem today is a widespread lack of understanding of software engineering approaches and tools for formal verification of source model verification, compiler toolchains, and binaries, and also a lack of diligence and effort in implementing rigorous practices.

Don’t forget Temple OS

> Eschew flamebait. Avoid generic tangents. Omit internet tropes.

https://news.ycombinator.com/newsguidelines.html

god seL4 everywhere would be awesome.