If you do try it, I'd encourage you to think of it as an exercise in formally documenting your code's behavior, with the side benefit that CrossHair can sometimes help you ensure the correctness of that documentation.
And, of course, feedback of any kind at all is honestly appreciated. Thanks for being the awesome community that you are!
This is an area I'm trying to focus my Masters on, so any opportunity to apply what I'm reading is more than welcome! I'll add my email to my profile if you'd like to chat.
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...
