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?