>AFAIK Linux RT kernel is designed to hit every deadline, but they just cannot offer a formal proof.

And that's why it is soft realtime. No guarantee, no hard realtime. It really is that simple.