What problem does it solve?
Writing formally verified MoonBit code requires coordinating abstract models, representation invariants, contracts, loop invariants, and solver guidance, and ad-hoc attempts often produce unprovable verification conditions or bloated trusted code. This Skill provides a disciplined workflow for structuring proof-carrying MoonBit packages so proofs actually go through.
Core Features & Use Cases
- Structured proof design: Separates proof-side logic (models, invariants, lemmas) into
.mbtp files from executable .mbt code with named *_pre / *_post contract predicates.
- Solver guidance patterns: Provides concrete techniques for
proof_assert placement, loop proof_invariant and proof_yield annotations, extensional equality lemmas for sets/maps, and staged concrete-update predicates for packed representations.
- Proof debugging workflow: Classifies failures from
moon prove output and _build/verif/<pkg>/<pkg>.proof.json into missing facts, bad quantifier instantiation, solver perturbation, or frontend lowering limits, with matching fixes.
- Use Case: When implementing a verified sparse array or AVL tree in MoonBit, use this Skill to define the abstract
model(...), keep the invariant small, write loop invariants early, and shrink trusted proof_axiomatized bridges step by step.
Quick Start
Use the moonbit-proof skill to add verified contracts and invariants to my MoonBit hash set implementation and get moon prove passing.
