Supporting Resources
Standard Library and Framework Specifications
Section titled “Standard Library and Framework Specifications”Examples
Section titled “Examples”hello_proverexamplebasic-coinexamplemath-puzzleexamplerounding-errorexampleverify-sortexample- Move Prover Examples by Zellic
Tutorials
Section titled “Tutorials”- The Move Tutorial, steps 7 and 8
- Verify Smart Contracts in Aptos with the Move Prover by MoveBit
- The Move Prover: A Practical Guide by OtterSec
- Formal Verification, the Move Language, and the Move Prover by Certik
- The Move Prover: Quality Assurance of Formal Verification by Certik
Presentations
Section titled “Presentations”- Verifying Smart Contracts with Move Prover by Wolfgang Grieskamp (video)
- Formal verification of Move programs for the Libra blockchain by David Dill (video)
- Move Prover - Best Practices & Tricks - A User’s Perspective by Xu-Dong@MoveBit (slides)
Conference papers
Section titled “Conference papers”- Zhong, Jingyi Emma, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark Barrett, and David L. Dill. “The move prover.” In International Conference on Computer Aided Verification, pp. 137-150. Springer, Cham, 2020.Harvard
- Dill, David, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, and Emma Zhong. “Fast and reliable formal verification of smart contracts with the Move prover.” In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 183-200. Springer, Cham, 2022.Harvard
- Park, Junkil, Teng Zhang, Wolfgang Grieskamp, Meng Xu, Gerardo Di Giacomo, Kundu Chen, Yi Lu, and Robert Chen. “Securing Aptos framework with formal verification.” In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2024.