Static verification

Contracts and refinements 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.

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:

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 executes a program.

Read the result, not just the exit codeCopy Anchor Link

• 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 buildCopy Anchor Link

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 for solver budgets, JSON fields, cache authentication and manifest statuses.

NextCopy Anchor Link

Testing: deterministic examples, properties and replay.