#MoonBit Formal Verification with moon prove

#How it works

 .mbt + .mbtp          moonc prove             Why3 + Z3
┌────────────┐      ┌──────────────┐      ┌──────────────┐
│ Source code │ ───► │ Generate     │ ───► │ Prove goals  │
│ + predicates│      │ WhyML (.mlw) │      │ via SMT      │
└────────────┘      └──────────────┘      └──────────────┘

#1. User writes specifications

• .mbt — MoonBit code with contracts and loop invariants
• .mbtp — Predicate definitions used in contracts

predicate in_bounds(xs : FixedArray[Int], i : Int) {
  (0 <= i) && (i < xs.length())
}

predicate sorted(xs : FixedArray[Int]) {
   i : Int,  j : Int,
    ((in_bounds(xs, i)) && (in_bounds(xs, j)) && (i <= j)) 
      xs[i] <= xs[j]
}

pub fn lower_bound(xs : FixedArray[Int], key : Int) -> Int  {
  proof_require: sorted(xs),
  proof_ensure: result => lower_bound_ok(xs, key, result),
} {
  for lo = 0, hi = xs.length(); lo < hi; {
    let mid = lo + (hi - lo) / 2
    if xs[mid] < key {
      continue mid + 1, hi
    } else {
      continue lo, mid
    }
  }  {
    lo
  }  {
    proof_invariant: 0 <= lo,
    proof_invariant: lo <= hi,
    proof_invariant: hi <= xs.length(),
    proof_invariant: all_less_before(xs, key, lo),
    proof_invariant: all_geq_from(xs, key, hi),
  }
}

• proof_require: pred(...) — precondition (assumed true on entry), in the function's own where clause, written after the return type
• proof_ensure: result => pred(..., result) — postcondition (must hold on exit); the lambda parameter names the return value
• where { proof_invariant: expr, ... } — loop invariants (must hold at every iteration boundary)
• proof_reasoning: (#| ...) — a human-readable proof sketch attached to a loop's where clause

#2. Lowering to WhyML

#3. Proving with Why3 + Z3

• Loop invariant initialization — invariant holds before the first iteration
• Loop invariant preservation — if invariant holds before an iteration and the loop condition is true, it holds after the iteration body
• Postcondition — the ensures clause holds when the function returns
• Termination — the variant decreases and stays non-negative
• Array bounds — array accesses are within bounds

Z3 @ 0.2s, 1000 MB   →  quick wins
Z3 @ 1s,   1000 MB   →  moderate goals
compute_specified      →  unfold definitions
split_vc               →  break conjunction goals apart
Z3 @ 2s,   4000 MB   →  harder goals

#Running

moon prove

#Examples

#Branch-only proofs

#Search, witness extraction, and partition proofs

• predecessor_search proves a full split: everything up to result is <= key, everything after is > key.
• bit_partition_point is a specialized lower-bound proof over monotone 0/1 arrays.
• rotation_pivot and mountain_peak use binary search to recover structural boundaries in nontrivial array shapes.
• closest_zero_sorted, closest_key_sorted, and closest_key_total prove global nearest-neighbor witness properties from binary-search splits, including the endpoint cases where the key lies outside the array range.
• last_key_sorted proves a last-occurrence witness via upper-bound search.
• closest_pair_sorted proves the classic theorem that, in a sorted array, a globally closest pair can be taken to be adjacent.
• first_descent and first_duplicate_sorted return concrete witnesses rather than boolean flags.

#Closed-form sums and sequence identities

• sum_cubes, sum_fourth_powers, sum_fifth_powers, sum_sixth_powers, sum_seventh_powers, sum_eighth_powers, sum_ninth_powers, sum_tenth_powers, sum_eleventh_powers, odd_squares, sum_triples, and odd_cubes all use nonlinear polynomial invariants with exact postconditions.
• cassini, pell_cassini, and lucas_cassini prove alternating-sign identities over three different recurrence-derived quadratic forms.
• cauchy2 through cauchy34 prove exact Cauchy-Schwarz identities in dimensions 2 through 34, not just the final nonnegativity inequality.
• lagrange4sq proves Lagrange's four-square identity, i.e. norm multiplicativity for quaternion-style multiplication.
• variance4 through variance36 prove exact finite-dimensional variance identities as sums of pairwise squares.

#Quantified array invariants and inequalities

• maxprofit and minmax_gap use quantified optimality/bounding arguments.
• abs_sum_dominates_each proves a computed value bounds every element's absolute value.
• tv_diameter strengthens total variation to an all-pairs bound over the entire array.
• telescoping_diff and total_variation show two different ways of proving endpoint facts from adjacent differences.

#Known limitations

1. Sequential continue assignment — continue i + 1, i sets the second variable to the updated i. Use a let binding to capture the old value.

2. proof_require / proof_ensure only accept predicate calls — inline expressions like proof_require: lo <= hi are a syntax error. Define a named predicate in .mbtp.

3. ∀ must be at the top level of a predicate body — cannot be nested inside &&. Move conditions into the implication consequent instead.

4. Loop variant requires loopvar < expr condition — conditions like r >= b or lo + 1 < hi produce no termination variant. Use lo < hi - 1 (recognized as loopvar < expr) or restructure the algorithm.