MoonBit Proof-Carrying Code

Use this skill when the task is to write, extend, or debug verified MoonBit code.

Typical triggers:

• add contracts to executable MoonBit code
• define an abstract model or representation invariant
• verify a recursive data structure
• connect a concrete representation to a set/map model
• replace trusted proof bridges with lemmas
• debug proof failures, timeouts, or frontend lowering limits

Goal

Write proof-carrying code, not proof-shaped comments.