Proverbot9001 is an ongoing project to prove theorems in Coq automatically using machine learning and neural networks. Proverbot9001’s goal is to make foundationally verifying software more accessible to more software projects.

Proverbot9001 is free software (free as in freedom, but you also don’t need to pay anything), and is publicly available on Github. It’s still a work in progress, and as such might not be easy to set up on every machine. If you’d like to contribute, please get in touch, or send a pull request!

You can find out more about Proverbot9001 from our extended paper (the short version was published at MAPL 2020). You can also watch the talk in the full MAPL proceedings.

Proverbot9001 is a collaboration of Alex Sanchez-Stern, Yousef Alhessi, Sicun Gao, Lawrence Saul, and Sorin Lerner at UC San Diego.