I am not at all against formal verification. In fact, I evangelize it and use it myself quite a bit. But it is important to understand that it is very, very far

I am not at all against formal verification. In fact, I evangelize it and use it myself quite a bit. But it is important to understand that it is very, very far from being a miracle cure. All software proofs prove correctness of specific theorems about a program given certain axioms. Those axioms must include, at the very least, the conformance of the hardware to some specification. But hardware can, at best, conform to the specification with some probability. For example, when you write `mov rax, [rdx]` it is not true that the computer will, 100% move the contents of the address pointed to by rdx into rax, only that it will do so with some high probability. Therefore, any proof about a software system (as opposed to an algorithm, which is an abstract mathematical entity) is a proof of a theorem of the form, "as long as the system behaves according to my assumptions, it will exhibit behaviors consistent with my conclusions." And that is even assuming that your conclusions cover all possible attacks. As it is generally impossible to formalize the concept of an arbitrary attack, you generally prove something far weaker. But none of this is even the biggest limitation of formal verification. The biggest would be its cost and lack of scalability. seL4 is about 1/5 the size of jQuery, and it is probably the largest piece of software ever verified end-to-end using deductive formal proofs as a verification technique. However much the effort of a similar technique can be reduced, it doesn't scale linearly with the size of the program (it may if the program does the same things, but usually larger programs are much more complex and have many more features).