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?
Sure, every little bit helps. But, keep in mind formal verification isn’t going to prevent configuration errors, and it remains to be seen if, for example, automated verifiers can do anything like the sel4 proof at scale. sel4 is tiny compared to most other software systems. There will still be technical avenues to attack, and if those get closed off nation state actors will just go back to spying the old fashioned way.
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?