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.