Even with the "guarantees" offered by e.g. seL4, you still need cooperating hardware. SMIs on most mobos cannot be masked, and can take an eternity to be handled by the BIOS.

Fortunately, for realtime audio, you don't need hard realtime unless you're very close to overloading the CPUs. Soft realtime (i.e. 99% of all interrupts handled within N usecs, 100% handled with N*2) is good enough.