I'm a fan. I've been building a proof assistant directly on the z3py api. https://pypi.org/project/knuckledragger/0.1.3/