While I agree with you in principal and am sympathetic to your position, it is not the case that security is "absolute" without taking threat model into account. As a specific example, SeL4 does not take timing channel vulnerabilities into account.

If you are doing formal verification, then you can make your own model, create software and attempt to prove that the software has issues within that model. seL4 is just one example of someone doing that.

Uh, I know. My point is that you won't always know all the security vectors you have to deal with. There's no way of just asserting that your model is free of side-channel attacks without (minimally) intimate knowledge of the hardware it's going to run on.