TL;DR Trillions of dollars are locked into blockchains, and hackers may exploit vulnerabilities in them. Thus, key blockchain components must be well-tested before deployment. However, standard testing/audit techniques are not enough for high levels of assurance. We explore using formal verification to achieve provable security in our blockchain