> Ordinary testing using a few handpicked example
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.
I think I cover what you're suggesting in my final paragraph?
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.