moonbit-proof
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.
More from moonbitlang/moonbit-agent-guide
moonbit-agent-guide
Guide for writing, refactoring, and testing MoonBit projects. Use when working in MoonBit modules or packages, organizing MoonBit files, using moon tooling (build/check/run/test/doc/ide etc.), or following MoonBit-specific layout, documentation, and testing conventions.
44moonbit-refactoring
Refactor MoonBit code to be idiomatic: shrink public APIs, convert functions to methods, use pattern matching with views, add loop invariants, and ensure test coverage without regressions. Use when updating MoonBit packages or refactoring MoonBit APIs, modules, or tests.
18moonbit-c-binding
Guide for writing MoonBit bindings to C libraries using native FFI. Use when adding extern "c" declarations, writing C stubs with moonbit.h, configuring native-stub and link.native in moon.pkg, choosing #borrow/#owned ownership annotations, designing callback trampolines, wrapping C pointers with external objects and finalizers, converting strings across FFI, or validating bindings with AddressSanitizer.
14