Move

Checking Move Code

Use the {{ tool(name="move_package_status") }} MCP tool to check for compilation errors and warnings.

• Call {{ tool(name="move_package_status") }} with package_path set to the package directory.
• The tool sets error and returns detailed error messages if the package does not compile.

Notice that like with a build system, the tool is idempotent, and does not cause recompilation if the compilation result and sources are up-to-date.

Edit–Compile Cycle

When fixing compilation errors, follow this iterative loop:

1. Call {{ tool(name="move_package_status") }} with the package path.
2. If the package compiles cleanly, report success and stop.
3. If there are errors, read the diagnostics carefully, fix the source, and go back to step 1.

Package Information

Use the {{ tool(name="move_package_manifest") }} MCP tool to discover source files and dependencies of a Move package:

• Call {{ tool(name="move_package_manifest") }} with package_path set to the package directory.
• The result includes source_paths (target modules) and dep_paths (dependencies).

Formal Verification

Use the {{ tool(name="move_package_verify") }} MCP tool to run the Move Prover on a package and formally verify its specifications:

• Call {{ tool(name="move_package_verify") }} with package_path set to the package directory.
• The tool returns "verification succeeded" when all specs hold, or a diagnostic with a counterexample when a spec fails.

Narrowing scope with filters

Verification of a full package can be slow. Use the filter parameter to restrict the prover to only the code you are working on:

• Single function: set filter to module_name::function_name to verify one function.
• Single module: set filter to module_name to verify all functions in one module.

A good workflow when writing or editing specs is:

1. Start with a function-level filter to get fast feedback on the spec you are editing.
2. Once the function verifies, widen to the module to catch any interactions.
3. Finally, run without a filter to verify the whole package.

Adjusting the timeout

The timeout parameter controls the solver timeout per verification condition (default: 40 seconds). Useful strategies:

• Use a short timeout (5–10 s) during iterative editing to get quick feedback. If the prover cannot decide within the limit it will report a timeout error; combine with a function-level filter for the fastest cycle.
• Increase the timeout (60–120 s) for complex specs that involve heavy arithmetic, loops, or large data structures.
• If verification times out repeatedly, consider simplifying the spec or adding helper lemmas rather than increasing the timeout further.

Turning Verification Off

If a verification timeout cannot be resolved, then as a last resort, the verification of the related function can be disabled by adding pragma verify = false; to the spec block.

Edit–Verify Cycle

When writing or fixing specifications, follow this iterative loop:

1. Call {{ tool(name="move_package_verify") }} with the package path. Use a filter for the function or module you are working on and a short timeout (5–10 s) for fast feedback.
2. If verification succeeds, widen the filter (function → module → full package) and re-verify.
3. If verification fails with a counterexample, read the diagnostics, fix the spec or implementation, and go back to step 1.
4. If the same function times out twice in a row, add pragma verify = false; to its spec block and move on.

Rules

• When you edit specifications, do not introduce pragma aborts_if_is_partial. Do not weaken specifications.