sui-prover

Run `npx skills add asymptotic-code/sui-prover --all -g -y` in your terminal to install the skill globally. The prover binary itself can also be installed via Homebrew with `brew install asymptotic-code/sui-prover/sui-prover`.

It formally verifies Move smart contracts on the Sui blockchain, mathematically proving that your code meets its specifications and cannot abort unexpectedly. It uses the Boogie verification engine and the Z3 solver under the hood.

Create a spec function annotated with `#[spec(prove, target = ...)]` in a sibling Move package, using `requires` for preconditions and `ensures` for postconditions. Then run `sui-prover --path ./specs` to verify it.

Add the `focus` attribute to verify only that spec, then run with `--verbose` to see counterexamples and execution traces. 'Code aborts' errors mean missing asserts, while 'Assert does not hold' means the condition logic needs fixing.

Yes. The included skill lets your agent write specifications, run the prover, and debug verification failures directly from natural language requests.