I’ve been building model based properties with quixir for a while. It works pretty well. Granted, you have to build pre-condition and post-condition checking yourself and the shrinking is much less optimized for model properties then eqc. Plus you don’t get the PULSE scheduler for inducing and controlling race-conditions which is really the most critical piece IMO.
