Rather, formal verification is just one piece in the puzzle. The software responsible for contracts in Ethereum needs to be equally well and thoroughly developed as if it was sending people to the Moon in the 60s or to Mars in the current Decade.
It'll probably take blood, sweat, money and mistakes just like in many other disciplines but we'll get there.
What problems specific to Ethereum do you see? Formal verification has been applied to complex domains and large projects before.
Work on this has indeed been going on for decades, and its very limited adoption so far is a testament to its difficulty. Only a tiny fraction of the code in the domains you mention is formally verified, and I notice that banking and finance are not on your list. The answer to "why would how useful Ethereum is or could be make a difference?" is that if Ethereum becomes as useful and important as intended, the size and scope of the problem will be well beyond anything that has been achieved so far. Arguably, given the value at risk, it has already crossed that threshold by a wide margin.
There are, however, people working on it, such as at Cardano [1], which is an exciting development. Ultimately, I think it will be more successful than trying to fix Ethereum.
If you don't have experience writing formally-verified code, I suggest the F* tutorial [2].