Install the Move Prover

If you want to use the Move Prover, install the Move Prover dependencies after installing the CLI binary.

1. See Building Aptos From Source

2. Then, in the checked out aptos-core directory, install additional Move tools:

   Linux / macOS

   1. Open a Terminal session.
   2. Run the dev setup script to prepare your environment: ./scripts/dev_setup.sh -yp
   3. Update your current shell environment: source ~/.profile

   tip

   dev_setup.sh -p updates your ~./profile with environment variables to support the installed Move Prover tools. You may need to set .bash_profile or .zprofile or other setup files for your shell.

   Windows

   1. Open a PowerShell terminal as an administrator.
   2. Run the dev setup script to prepare your environment: PowerShell -ExecutionPolicy Bypass -File ./scripts/windows_dev_setup.ps1 -y

3. You can now run the Move Prover to prove an example:

   aptos move prove --package-dir aptos-move/move-examples/hello_prover/

Troubleshooting

If you encounter errors like the one below when running the command, double-check your Aptos CLI version or verify that you're using the correct aptos tool, especially if you have multiple versions installed.

error: unexpected token
    ┌─ ~/.move/https___github_com_aptos-labs_aptos-core_git_main/aptos-move/framework/aptos-framework/sources/randomness.move:515:16
    │
515 │         for (i in 0..n) {
    │             -  ^ Expected ')'
    │             │
    │             To match this '('

{
  "Error": "Move Prover failed: exiting with model building errors"
}