Parameterized unit tests are a form of property-based testing that generalizes traditional unit tests. The tests can be instantiated with concrete values to serve as traditional tests, they can be verified using symbolic execution or, to support modular verification, they can be used as axioms in the spirit of algebraic specification to use when verifying calls to a library.
This was implemented for .NET on an early symbolic execution tool using early SMT solvers. It is evaluated on eight benchmarks (qsort, triangle, hashtable, bad, linkedlist, red-black tree).
The paper has a lengthy related/future work section that cites lots of early (forgotten?) work on test generation from formal specifications from the ’90s.