Unambiguous requirements
First off, how exactly is finance "main" on any metric related to writing software? I argue that fields like automotive, defence, aerospace, telecommunications, and boring old general-purpose "software for everyone" are as significant, or more so, on most such metrics.
That said, I agree in part -- ambiguity of requirements is a huge problem. However, it's neither more nor less of a problem absent or present formal verification. Thus, even if verification buys you nothing on this point (not something of which I'm totally convinced), it doesn't matter -- what it does buy you is the guaranteed absence of certain classes of bugs. For example, the seL4 proof is of "functional correctness". That is, "the C implementation of the kernel does exactly what the spec says it does". Given that the spec does not permit the running code to change (ok, my wording is a little hazy here, verification isn't my forte), there are therefore no code injection bugs in the microkernel. In a similar vein, buffer overflows, unchecked arrays, and exceptions of any kind simply do not occur in any kernel code, and this is utterly guaranteed.
So even under ambiguous requirements, the kinds of bugs that give rise to embarassing security holes with multi-million-dollar fixes (hello Windows, Linux, etc) are verified not to exist. This is a statement that otherwise cannot be made about any reasonably-sized codebase.
