Clojurians Log v2

I'm getting into alloy and tla+, and a naive idea came to my mind: what if we replace test.check with a sat solver for spec/malli? Basically, test.check is for random testing, which is great for finding bugs, but we are essentially building a model for our code using it anyway. It finds minimal examples, but it's not for low-probability combinations, and a sat solver could shine here, if I'm not totally wrong. Can we avoid building two separate models: for random testing and for finding deep counterexamples? Is this feasible?