This is essentially exactly what model checkers do. The big difference is that they exploit the structure of the problem description in order to reach exhaustiv

This is essentially exactly what model checkers do. The big difference is that they exploit the structure of the problem description in order to reach exhaustiveness in “reasonable” time. This can be a big time saver over trying to do it manually. I’d emphasize that using Alloy/TLA is often an iterative process where you refine your model over time. In this way, it’s possibly faster to dig through several iterations in Alloy before identifying a counter-example to a property of interest. But if you are mostly interested in finding interesting test sets then you should be able to stop once you’ve modeled your actual implementation well enough.