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.