Verified worst case execution time analysis. So instead of just hanging on it until it achieves the desired responsiveness (like QNX and rt Linux) Sel4 can actually back up its claim.