Disclosure - I used to work in static analysis.
Abstract interpretation, as used by Polyspace and Absint, can indeed catch more defects statically than "simple" static data-flow analysis. However, decidability means that abstract interpretation is still not able to detect all errors. SPARK helps by limiting the features of the language that are permitted (it defines a language subset). Subsetting is very difficult to enforce within the C and C++ communities as there is a lot of pushback from developers who don't like being told that they are not to use (often large) parts of "their" language.
Formal verification is a good idea,but only a relatively small number of programmers understand that it exists, and even less understand how to use it. There is also a concern that you can end up with a vacuous proof (you've proved something, but did you really prove that the software is correct?), <a href="https://blogs.sw.siemens.com/verificationhorizons/2017/12/06/formal-tech-tip-what-are-vacuous-proofs-why-they-are-bad-and-how-to-fix-them/>but that's another story</a>...
However, the use of tools is essential as they help to improve the confidence in a system, even when they cannot prove that it is correct.