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.
In that case, you’re just hanging on the specs, prover, compiler, and other dependencies. Things most developers can’t even begin to verify. That also assumes the hardware works which isn’t safe if talking about cosmic rays.
Empirical testing of “verified” software often found errors, too. High-assurance, security certification used to require formal methods, thorough testing of code, review of anrtifacts, and pen testing by independent team. We should do that today.
In this case, you’d do white box and black box testing of the WCETS of seL4.
