sui-prover

Sui Prover

Help the user with the Sui Prover -- running verification, writing specifications, debugging failures, and understanding results. If arguments are provided, incorporate them. For the full specification API reference (math types, vector iterators, attributes), see spec-reference.md.

Installation

brew install asymptotic-code/sui-prover/sui-prover

Move.toml Setup

The Sui Prover relies on implicit dependencies. Remove any direct dependencies to Sui and MoveStdlib from Move.toml:

# DELETE this line if present:
Sui = { git = "https://github.com/MystenLabs/sui.git", subdir = "crates/sui-framework/packages/sui-framework", rev = "framework/testnet", override = true }

Keep prover specifications and prover-specific dependencies in a sibling Move package next to the implementation package.

Running the Prover

Run from the directory containing Move.toml:

sui-prover
sui-prover --path ./my_project
sui-prover --verbose --timeout 60

If the user provides arguments like $ARGUMENTS, pass them to sui-prover directly.

Writing Specifications

Write specification modules in a sibling Move package that depends on the implementation package. To verify an implementation function, write a specification function annotated with #[spec(prove, target = ...)]. The spec has the same signature as the function under test and follows this structure:

#[spec(prove, target = project::example::my_function)]
fun my_function_spec(args): ReturnType {
    // 1. Preconditions assumed on arguments
    requires(precondition);

    // 2. Capture old state if needed
    let old_state = clone!(mutable_ref);

    // 3. Call the function under test
    let result = project::example::my_function(args);

    // 4. Postconditions that must hold
    ensures(postcondition);

    // 5. Return the result
    result
}

How Specs Compose

• External target: Every spec for an implementation function must use target = <implementation-path> because the spec lives in a sibling package.
• prove: The spec is verified by the prover. Without prove, the spec is not checked itself, but is still used when proving other functions that depend on it.
• focus: Only verify this spec (and other focused specs). Useful for debugging. Do not commit focus — it skips all non-focused specs.
• no_opaque: By default, the prover can use the external spec targeting a called function as an opaque summary. Adding no_opaque forces the prover to include the actual implementation instead.
• Scenario specs: A spec without a target attribute is a standalone scenario — it is verified but does not specify an implementation function.