Check it out: https://www.philipzucker.com/state_o_knuck/ The dude is adopting Z3 solver for Python 🕺 So far, its quite promising. Hopefully, it will continue to thrive 💪