Very cool! Ever looked at the Viper project? It's the only other system in python that I know of targeting pre and post conditions https://www.pm.inf.ethz.ch/r

Very cool! Ever looked at the Viper project? It's the only other system in python that I know of targeting pre and post conditions https://www.pm.inf.ethz.ch/research/viper.html https://www.pm.inf.ethz.ch/research/viper.html https://www.pm.inf.ethz.ch/research/nagini.html https://www.pm.inf.ethz.ch/research/nagini.html Another thing that might be of interest is HOLpy. I have no idea what the state of that is. https://arxiv.org/abs/1905.05970 https://arxiv.org/abs/1905.05970 I was fiddling around recently with way jankier methods than what you've done here http://www.philipzucker.com/programming-and-interactive-proving-with-z3py/ http://www.philipzucker.com/programming-and-interactive-prov...