My post: I used the Z3 SMT solver to test if two models are logically equivalent across the entire input space (not just in the sample data). It either finds a counterexample or proves none exists. To be considered when simplifying complex models or when retraining routines in mlops. Post includes code and discussion.