Proves a Move Package

This is a tool for formal verification of a Move package using the Move prover.


movement aptos move prove [OPTIONS]


  • --dev Enables dev mode, which uses all dev-addresses and dev-dependencies. Dev mode allows for changing dependencies and addresses to the preset [dev-addresses] and [dev-dependencies] fields. This works both inside and out of tests for using preset values. Currently, it also additionally pulls in all test compilation artifacts.

  • --package-dir <PACKAGE_DIR> Path to a move package (the folder with a Move.toml file).

  • --output-dir <OUTPUT_DIR> Path to save the compiled move package. Defaults to <package_dir>/build.

  • --named-addresses <NAMED_ADDRESSES> Named addresses for the move binary. Example: alice=0x1234, bob=0x5678. Note: This will fail if there are duplicates in the Move.toml file remove those first. [default: ]

  • --skip-fetch-latest-git-deps Skip pulling the latest git dependencies. This will allow overriding this for local development.

  • --bytecode-version <BYTECODE_VERSION> Specify the version of the bytecode the compiler is going to emit.

  • -v, --verbosity <VERBOSITY> Verbosity level.

  • -f, --filter <FILTER> Filters targets out from the package. Any module with a matching file name will be a target, similar as with cargo test.

  • -t, --trace Whether to display additional information in error reports. This may help debugging but also can make verification slower.

  • --cvc5 Whether to use cvc5 as the smt solver backend. The environment variable CVC5_EXE should point to the binary.

  • --stratification-depth <STRATIFICATION_DEPTH> The depth until which stratified functions are expanded. [default: 6]

  • --random-seed <RANDOM_SEED> A seed for the prover. [default: 0]

  • --proc-cores <PROC_CORES> The number of cores to use for parallel processing of verification conditions. [default: 4]

  • --vc-timeout <VC_TIMEOUT> A (soft) timeout for the solver, per verification condition, in seconds. [default: 40]

  • --check-inconsistency Whether to check consistency of specs by injecting impossible assertions.

  • --keep-loops Whether to keep loops as they are and pass them on to the underlying solver.

  • --loop-unroll <LOOP_UNROLL> Number of iterations to unroll loops.

  • --stable-test-output Whether output for e.g. diagnosis shall be stable/redacted so it can be used in test output.

  • --dump Whether to dump intermediate step results to files.

Last updated