At least in the TLA+ community, the new state-of-art approach is to use the formal model to generate a test suite.