[philzook]

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/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

I was fiddling around recently with way jankier methods than what you've done here http://www.philipzucker.com/programming-and-interactive-prov...