# Static verification

URL: /docs/tour/verification
Markdown: /docs/tour/verification.md

> Check contracts before execution and distinguish proofs from runtime checks.

[Contracts and refinements](/docs/tour/contracts) check values at runtime. The source-built CLI also provides `sakura verify`: it asks a separately installed, pinned Z3 **5.3.1** to check contract and arithmetic obligations before execution. This is a pre-alpha preview, not a whole-program correctness guarantee.

```sakura
fn clamp(x: Int, lo: Int, hi: Int) -> Int
  requires ordered: lo <= hi
  ensures bounded: lo <= result && result <= hi
{
  if x < lo { lo } else if x > hi { hi } else { x }
}

pub fn main() -> Unit {
  let _value = clamp(12, 0, 10)
}
```

Save this as `main.sakura`, then run:

```sh
sakura verify main.sakura
sakura verify --json main.sakura
sakura verify --target wasm main.sakura
```

The example proves two obligations: this call meets `ordered`, and `clamp` meets `bounded` on normal return assuming its precondition. The default profile is JavaScript's safe-integer range; `--target wasm` checks signed i64 arithmetic. It selects a verification profile; [`run --target wasm`](/docs/tour/memory#backends) executes a program.

## Read the result, not just the exit code [#read-the-result-not-just-the-exit-code]

- `proved`: holds under the recorded assumptions. `W7002` and `path_feasible: false` flag a vacuous proof whose assumptions cannot hold.
- `disproved`: a counterexample exists. Inspect `replay` to distinguish a confirmed JS execution from a candidate; i64 replay remains planned.
- `unknown`: the solver could not decide within its limits, or encountered a solver failure.
- `unsupported`: the obligation is outside the implemented fragment.

A completed run exits 1 for any `disproved` obligation and otherwise 0, including `unknown` and `unsupported`. Setup and compilation errors can also fail. Automation requiring all proofs must inspect the JSON Lines records. A postcondition can hold on normal return while a separate multiplication-overflow obligation fails; proving one does not prove the other.

## What changes in a build [#what-changes-in-a-build]

```sh
sakura build --manifest main.sakura
```

JS builds can remove eligible `ensures` and non-entry `where` checks using matching authenticated proof records. Missing or stale records retain checks. This does not remove preconditions or `T.from` entry checks, and the predicate's computation remains. `run`, `test`, LIR output and WASM builds retain these checks. Separate interval-based arithmetic optimization does not require the solver.

Verification of loops, recursion, termination, quantified collections and Float/String theories remains planned. Proof certificates and `verify fn`, `proof` and `ghost` syntax are not implemented. Read the [verification reference](/docs/agents/verify) for solver budgets, JSON fields, cache authentication and manifest statuses.

## Next [#next]

[Testing](/docs/tour/testing): deterministic examples, properties and replay.