From moonbit-skills
Writes and debugs proof-carrying code in MoonBit with Why3-backed specifications, abstraction functions, representation invariants, and proof assertions.
How this skill is triggered — by the user, by Claude, or both
Slash command
/moonbit-skills:moonbit-proofThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
Use this skill when the task is to write, extend, or debug verified MoonBit code.
Use this skill when the task is to write, extend, or debug verified MoonBit code.
Typical triggers:
Write proof-carrying code, not proof-shaped comments.
That means:
proof_assert steps explain why the implementation satisfies the modelPrefer model(...) as the default name for the proof-side semantic view of a value.
Examples:
model(set) : Fset[Int]model(map) : Fmap[Int, Int]model(tree) : Seq[Int]Use a more specific name only when it is materially clearer:
elements(node) when the model is literally the set of elements stored in a recursive subtreedomain(bitmap) when the model is specifically the occupied index setheight(tree) when it is a structural measure, not the main semantic modelDefault rule:
model for the main semantic abstractionelements, domain, height, or rank for auxiliary viewsSplit the package into two layers.
.mbtp
model(x)tree_inv(x) or sparse_array_inv(x)insert_pre(...) and insert_post(...).mbt
proof_assert steps after construction, branching, and loopsUse this default unless there is a strong reason not to.
*_pre / *_post predicates.proof_assert steps where the solver needs help.Do not start by writing a large pile of lemmas.
Prefer the simplest model that matches the observable behavior.
model(node) or, if clearer, elements(node).Example:
fn model(set : HashSet) -> Fset[Int] {
match set.root {
None => @fset.fset_empty()
Some(node) => model(node)
}
}
If a recursive helper really denotes the element set of a subtree, this is also reasonable:
fn elements(node : Node) -> Fset[Int] {
match node {
Empty => @fset.fset_empty()
Branch(l, x, r) => elements(l).union(elements(r)).add(x)
}
}
Avoid putting the whole semantics directly into every contract.
The invariant should mostly describe:
Semantic equalities usually belong in postconditions or lemmas, not inside *_inv.
Good:
predicate sparse_ok(sa : SparseArray) {
sa.data.length() == count_value(sa.bitmap, 0) &&
(∀ i : Int,
valid_idx(i) && mem_value(sa.bitmap, i) →
0 <= rank_value(sa.bitmap, i, 0) &&
rank_value(sa.bitmap, i, 0) < sa.data.length())
}
Not good:
*_invPrefer named predicates over repeating large formulas. As a default naming convention, use *_inv, *_pre, and *_post.
Good:
predicate singleton_post(res : SparseArray, idx : Int, value : Int) {
sparse_ok(res) &&
model(res).eq(@fmap.fmap_empty().add(idx, value))
}
pub fn singleton(idx : Int, value : Int) -> SparseArray where {
proof_require: valid_idx(idx),
proof_ensure: result => singleton_post(result, idx, value),
} {
...
}
This keeps contracts short and gives the solver a reusable target.
.mbtpProof-side material belongs in .mbtp.
Examples:
fn model(t : Tree) -> Fset[Int] {
match t {
Empty => @fset.fset_empty()
Node(l, x, r, _) => model(l).union(model(r)).add(x)
}
}
predicate avl(t : Tree) {
match t {
Empty => true
Node(l, x, r, h) =>
avl(l) &&
avl(r) &&
all_lt(model(l), x) &&
all_gt(x, model(r)) &&
h == 1 + max2(height(l), height(r))
}
}
Keep .mbtp focused on:
Avoid filling .mbtp with runtime implementation details.
Two recurring helper patterns are especially useful:
Example:
predicate fmap_eq_hyp(m1 : Fmap[Int, Int], m2 : Fmap[Int, Int]) {
(∀ k : Int, m1.mem(k) == m2.mem(k)) &&
(∀ k : Int, m1.mem(k) → m1.find(k) == m2.find(k))
}
lemma fmap_eq_intro(m1 : Fmap[Int, Int], m2 : Fmap[Int, Int]) where {
proof_require: fmap_eq_hyp(m1, m2),
proof_ensure: m1.eq(m2),
} {
}
This is often the cleanest way to finish map-refinement proofs.
Examples:
mem at self and other keysfind at self and other keysPrefer several small transport lemmas over one giant “everything changed correctly” theorem.
.mbtAfter constructing data, assert the concrete facts the solver may miss.
Example:
let data = FixedArray::make(1, value)
proof_assert data.length() == 1
proof_assert data[0] == value
let result = { bitmap, data }
proof_assert sparse_ok(result)
proof_assert singleton_post(result, idx, value)
result
Use proof_assert:
Prefer this over introducing a callable trusted wrapper function.
Any loop that is relevant to the proof should get invariants as soon as the loop shape stabilizes.
In practice, proof-carrying MoonBit code often relies on loops for:
Do not wait for the prover to fail before writing the obvious invariants.
Typical invariants:
Example:
for j = 0, acc = 0; j < idx; {
let next_acc = if bitmap_mem(bitmap, j) { acc + 1 } else { acc }
proof_assert next_acc == rank_value(bitmap, j + 1, 0)
continue j + 1, next_acc
} nobreak {
acc
} where {
proof_invariant: 0 <= j,
proof_invariant: j <= idx,
proof_invariant: acc == rank_value(bitmap, j, 0),
}
For array updates, use staged invariants that match the proof shape.
Example:
for i = 0; i < pos; {
new_data[i] = old_data[i]
continue i + 1
} where {
proof_invariant: 0 <= i,
proof_invariant: i <= pos,
proof_invariant: add_prefix_ok(old_data, new_data, pos, i),
}
Then strengthen to a second invariant after the inserted/removed element is handled.
Default rule:
proof_yield so the prover knows what the yielded result satisfiesExample:
for i = 0, acc = 0; i < xs.length(); {
continue i + 1, acc + xs[i]
} nobreak {
acc
} where {
proof_invariant: 0 <= i,
proof_invariant: i <= xs.length(),
proof_invariant: acc == prefix_sum(xs, i),
proof_yield: res => res == prefix_sum(xs, xs.length()),
}
Use proof_yield when the proof needs a fact about the value produced by the whole loop expression, not just the state maintained during iteration.
If the public API is method-oriented, verify the methods directly.
Example:
pub fn HashSet::contains(self : HashSet, key : Int) -> Bool where {
proof_require: set_inv(self),
proof_ensure: result => result == model(self).mem(key),
} {
...
}
Use top-level verified helper functions only when they improve structure or reuse, not as a workaround for method contracts.
For recursive data structures:
model(node) or elements(node)node_ok(node, level)proof_decreaseExample:
fn contains_at(node : Node, key : Int, level : Int) -> Bool where {
proof_decrease: node,
proof_require: node_ok(node, level),
proof_ensure: result => result == model(node).mem(key),
} {
match node {
Flat(k) => key == k
Branch(children) => ...
}
}
If the solver resists tail-recursive loops in contracted functions, try structurally recursive code first.
When a representation is packed, indexed, or incrementally rebuilt, do not jump straight from low-level mutation to the final semantic theorem.
First prove concrete update facts that match the implementation structure, then connect them to the abstract model.
A common progression is:
*_post theoremThe exact intermediate predicates depend on the implementation. Choose names that reflect the actual stages in the code.
Typical stages are:
Example pattern:
predicate update_prefix_ok(before_data, after_data, upto) { ... }
predicate update_middle_ok(before_data, after_data, pos, value, upto) { ... }
predicate update_data_ok(before, key, value, after) { ... }
lemma update_model_lemma(...) where {
proof_require: update_data_ok(...),
proof_ensure: update_post(...),
} {
...
}
For sparse or dense-array code, a more specific ladder like *_prefix_ok, *_fill_ok, and *_data_ok is often effective, but treat that as one useful instance of the general technique rather than a universal template.
If you have reusable proof imports or theories, put them in shim packages.
Typical examples:
The benefit is:
But keep shared shims minimal. Large shared lemma sets can perturb unrelated proofs.
Also account for lowering quirks:
fmap_mk(...) may still be needed even if Fmap::mk(...) parsesIf a helper is only needed by one package, prefer a local lemma there rather than exporting it from a shared shim.
Trusted helpers are acceptable as narrow bridges, but they should not be the design endpoint.
If trust is unavoidable:
.mbtpGood temporary bridge:
fn singleton_bridge(res : SparseArray, idx : Int, value : Int) -> Unit where {
proof_axiomatized: true,
proof_require: valid_idx(idx),
proof_require: res.data.length() == 1,
proof_require: res.data[0] == value,
proof_ensure: singleton_ok(res, idx, value),
} {
()
}
Then remove trusted bridges in this order:
After a proof failure:
moon prove <pkg>_build/verif/<pkg>/<pkg>.proof.jsonClassify the problem before editing:
Different causes need different fixes.
Examples:
proof_assertCommon reproducer strategy:
moon check fails, moon prove crashes, or the VC merely times outAfter every proof edit:
moon check <pkg>
moon prove <pkg>
moon test <pkg> # if runtime code changed
After editing shared proof layers, rerun dependent packages too.
Do not assume a local fix is safe globally.
Avoid:
#proof_import in every client package.mbt functionsBefore handing off a verified MoonBit change, confirm:
model(...) exists, or there is a clear reason to use a more specific name like elements(...)*_inv predicate exists*_pre / *_post predicates when appropriate.mbtpproof_assert where neededproof_invariantmoon check, moon prove, and any needed moon test commands were runnpx claudepluginhub moonbitlang/skills --plugin moonbit-skillsGuides writing, refactoring, and testing MoonBit projects with moon tooling. Activates when working in MoonBit modules/packages or using moon build/check/test/doc/ide commands.
Enforces writing loop invariants, termination arguments, and edge cases before code to prevent subtle correctness bugs in algorithms like binary search, QuickSelect, and Boyer-Moore.
Enforces proof-driven development with formal verification using property-based testing, theorem proving, and proof tactics. Zero unproven properties in final code.