Move Prover Supporting Resources

Standard Library and Framework Specifications

• Move Stdlib
• Aptos Stdlib
• Aptos Framework
• Diem Framework

Examples

• hello_prover example
• basic-coin example
• math-puzzle example
• rounding-error example
• verify-sort example
• Move Prover Examples by Zellic

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

• 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

• 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
  • https://research.facebook.com/publications/the-move-prover/
• 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
  • https://research.facebook.com/publications/fast-and-reliable-formal-verification-of-smart-contracts-with-the-move-prover/