A useful practical way to look at formal methods is "just" as testing on steroids, rather than as competition for testing. The pros and cons are mostly the same: Depending very much on their skill level, the practitioner gets a definite but finite improvement in correctness and particularly resistance to regressions, for the cost of additional upfront time and ongoing friction during maintenance. The main difference is the amount of "punch" in each passing spec requirement, which can be equivalent to an infinite number of concrete passing tests. (In the other direction: Ordinary testing using a few handpicked example (input, expected output) pairs is formal verification, just of an especially thin kind.)
Sitting in between ordinary manual tests and formal verification of entire program properties is property-based testing like Haskell Quickcheck, which offer some of the benefits of both.
Ah, but if you have specifications, you should have the ability to generate unlimited numbers of tests. Handpicked examples aren't needed. The great advance in testing with increase in compute power was the realization that carefully handcrafted tests are silly; just blast huge amounts of randomness at the system and use cheap compute to save expensive human effort.
I think it's a common experience to implement some well-defined data structure or algorithm and use the clear specification of its behavior to randomly test it, to then discover this flushes out all the bugs.
Property-based testing is the automated spec-based random test generation you describe. It's much easier to get underway than strong formal methods that try to actually prove properties of all possible execution traces, while using many of the same powerful declarative notations, and using abundant CPU horsepower.
> the realization that carefully handcrafted tests are silly
On the downside, property-based testing won't necessarily find tricky edge cases as reliably as an experienced engineer creating individual cases manually. Specific regressions are also good to keep as "point" tests.