When I went through a tech school cyber security program (10+ years ago now) we were told that the situation was "If Canada wants to hack you, it is improbable you can stop them. If the US wants to hack you, they will. Therefore we will not be focussing on strategies to counter nation state actors." It was a forgone conclusion that you would lose against them. I imagine the situation hasn't improved much in the last ten years.

Maybe not feasible now, but maybe it could be feasible at some point in the future if things are built on top of seL4 , with similar techniques used to demonstrate that the programs in question also have some desired security properties, building on the security properties the kernel has been proven to have?

Of course, one might still be concerned that the hardware that the software is running on, could be compromised. (A mathematical proof that a program behaves in a particular way, only works under the assumption that the thing that executes the program works as specified.) Maybe one could have some sort of cryptographic verification of correct execution in a way where the verifier could be a lot less computationally powerful while still providing high assurance that the computations were done correctly. And then, if the verifier can be a lot less powerful while still checking with high assurance that the computation was done correctly, then perhaps the verifier machine could be a lot simpler and easier to inspect, to confirm that it is honest?

> zero day procurement budgets bigger than most company market caps

do you mean they pay companies to put backdoors into products? or you mean they just go hunting for vulnerabilities. maybe both?