Formal verification is very cool and definitely has its uses (https://www.sigops.org/s/conferences/sosp/2009/papers/klein-...). From what I heard at least some chip manufacturers do formal verification of their chip designs.

But I don't think it scales to general-purpose programming. Most of the easy-to-verify conditions could (and should) be checked by asserts and unit tests. But there's a whole layer of complexity on top of that and in my experience it accounts for the bigger share of bugs.