>Who cares about formal guarantees Projection. You might not care, but extrapolating is a mistake. Public as well as private sector with high assurance needs

>Who cares about formal guarantees Projection. You might not care, but extrapolating is a mistake. Public as well as private sector with high assurance needs have gathered around seL4 foundation due to its proofs and technical excellence. >are much better Subjective. What is your criteria? >Fiasco can be real-time. Depends on your definition of real-time. Hard realtime requires guarantees that the deadlines will always be met. The only non-toy kernel that offers proof of WCET is seL4. If soft realtime is all you need, then Linux with PREEMPT_RT suffices.