#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)
• proof_ensure: result => pred(..., result) — postcondition (must hold on exit; result refers to the return value)
• where { proof_invariant: expr, ... } — loop invariants (must hold at every iteration boundary)

#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

#No loops (branch-only proofs)

#Simple loops

#Binary search variants

#Quantified invariants

#Investor-Grade Crypto / Finance Showcase

• stablecoin_engine — verified mint/repay/withdraw/liquidate flows with exact bad-debt resolution
• cpmm_swap — fee-adjusted constant-product AMM swap math with reserve-safety and invariant proofs
• ltv_lending — solvency-preserving lending operations with exact risk-buffer accounting
• batch_auction — verified uniform-price batch-auction frontier search
• risk_limits — earliest-breach risk monitor for bounded exposure envelopes
• vesting_stream — bounded token vesting and release logic
• threshold_multisig — exact threshold execution via counted approvals

#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. Contracts work best with named predicates — complex inline boolean expressions are brittle. Define a named predicate in .mbtp and reference it from proof_require / proof_ensure.

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.