Install the Move Prover

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

1. Install the latest Aptos CLI binary.

2. Execute the command aptos update prover-dependencies.

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
   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

After installation, you can run the Move Prover to prove an example:

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

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"
}