For the purposes of demonstrating the formal verification capability of Aptos, we build this tutorial about specifying your code by Aptos Move Prover. We hope through this project, you can learn and understand about formal verification techniques, and build your specifications to guarantee the safety of your Dapp.
Before we start, setting up the environment is necessary. The Move Prover (MVP) is integrated in the Aptos CLI, a command line tool for developing, debugging, deploying and operating on the Aptos Network. So what we need to do is to include the installation of the Aptos CLI and the dependencies for the MVP.
Four installation methods are provided; please choose the preferred one.
For Mac, the easiest way to install the Aptos CLI is with the package manager brew.
- Ensure you have brew installed.
- Execute the following commands to install client.
brew update brew install aptos
- Check if client is installed.
aptos help
For Windows, the easiest way to install the Aptos CLI tool is via Python script.
- Ensure you have python 3.6+ installed.
- Run the install script in PowerShell.
iwr "https://aptos.dev/scripts/install_cli.py" -useb | Select-Object -ExpandProperty Content | python3
- Update your PATH with the command looks something like the following one.
setx PATH "%PATH%;C:\Users\<your_account_name>\.aptoscli\bin"
- Check if client is installed.
aptos help
For Linux, the easiest way to install the Aptos CLI tool is via Python script.
- Ensure you have python 3.6+ installed.
- Run the install script in your terminal.
Or use the equivalent wget command:
curl -fsSL "https://aptos.dev/scripts/install_cli.py" | python3
wget -qO- "https://aptos.dev/scripts/install_cli.py" | python3
- Update your PATH with the command looks something like the following one.
echo 'export PATH=/usr/local/bin:$PATH' >> ~/.bashrc source ~/.bashrc
- Check if client is installed.
aptos help
If you need a specific version of the Aptos CLI, you can build it directly from the Aptos source code.
- Follow the steps to build Aptos from source here
- Ensure you have cargo installed.
- Build the CLI tool:.
The binary will be available at
cargo build --package aptos --profile cli.
target/cli/aptos
ortarget\cli\aptos.exe
. - (Optional) Move this executable to a place in your PATH.
- Check if client is installed.
Or
# for Linux/macOS target/cli/aptos help # for Windows target/cli/aptos.exe help
aptos help
If you want to use the Move Prover, install the Move Prover dependencies after installing the CLI binary.
-
Clone the Aptos repository.
git clone https://github.com/aptos-labs/aptos-core.git
-
Install dependencies.
For Linux/macOS
cd aptos-core/ ./scripts/dev_setup.sh -yp source ~/.profile
For Windows
PowerShell -ExecutionPolicy Bypass -File ./scripts/windows_dev_setup.ps1 -y
Note: Execute the Windows' command as an administrator!
If you’ve persisted up to this step, congratulations on completing the environment setup!