[throwawaylinux]

Preempt RT doesn't really give that. It might give that when you run a subset of Linux, but that is not Linux like nommu Linux is not Linux. They might say that's a bug, but there are countless algorithms and data structures in Linux that mean the state of the system and other workloads can slow down other parts of the system. Even setting aside the fact that a lower privileged process can take spin locks (not "preempt spinlocks" but real low level spin locks), disable interrupts, etc., they can influence shared data structures such that allocations, lookups, etc can take longer for the higher privileged thread. So you still end up with a "look we tried really hard and if you don't use any kernel facilities including blocking and isolate this CPU entirely, lock everything and don't allocate memory or take page faults after that, you might get something approaching hard-realtime".

People try to paint it as soft-hard-RT or something, but it's not, there already exists a good word for it which is soft-RT. Which is fine, it's highly useful.

There aren't really formally proven hard realtime operating systems of any non-trivial complexity are there? They are either extremely simple executive layers, or some very limited privileged functionality that sits on top of the rest of the kernel.

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