Overview
The Move Prover supports formal specification and verification of Move code. The Move Prover can automatically validate logical properties of Move smart contracts while offering a user experience similar to a type checker or linter.
The Move Prover exists to make contracts more trustworthy; it:
- Protects massive assets managed by the Aptos blockchain from smart contract bugs
- Protects against well-resourced adversaries
- Anticipates justified regulator scrutiny and compliance requirements
- Allows domain experts with a mathematical background, but not necessarily a software engineering background, to understand what smart contracts do
For more information, refer to the documentation: