[repolfx]

Sure, but if you look carefully most static analysis engines are developed by industry not academia because they're collections of heuristics that tend to work in practice rather than lots of clever-as-possible sounding theory.

But Hoare talks specifically about formal methods, which is widely understood to mean proving code meets a spec using techniques like constraint solvers. Dependent types may meet the definition too. And none of these techniques are used widely or have ever been used widely.