[AlotOfReading]

I'd highly recommend you read the link and the paper it's based on. It's pretty thorough in addressing the limitations. Those same limitations apply to virtually every commercial RTOS out there as well though.

As for formally verified systems, depends on your definition of "nontrivial". You can build complex systems from the building blocks provided by the well known examples like SeL4 and pikeos. On a practical level though, complete formal verification is incredibly uncommon for exactly the reasons you'd expect. There's usually a mix of formal methods and other verification methods employed in safety critical applications. It's "good enough" given current capabilities.

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