[throwawaylinux]

I did read it. I understand and work on Linux including real time Linux. Nothing of what I said is wrong. Hard realtime operating systems of course are more limited than general purpose Linux too, but they tend to have a much better handle on limiting and controlling latency and how non-critical workload can impact critical tasks.

And seL4 is formally verified but as far as I know it has not been formally verified for hard realtime. Funny thing about formal verification is that it's easy to do if you control the requirements :) (/s - nothing to take away from the incredible work of sel4). Last I heard people had sketched or theorized about ways it could be approached, but not done.