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.