用途：在 MoonBit 中编写、扩展或调试可验证代码，把运行时实现与其抽象模型连接起来，写出真正携带证明的代码而非“证明形状的注释”。典型触发场景包括给可执行 MoonBit 代码加契约、定义抽象模型或表示不变量、验证递归数据结构、把具体表示连接到集合/映射模型、用引理替换受信任的证明桥，以及调试证明失败、超时或前端 lowering 限制。
主要能力：建议以 model(...) 作为值的主要语义抽象，特殊视图才用 elements、domain、height 等专名；默认把包分为 .mbtp（模型函数、不变量 *_inv、命名谓词 _pre/_post、可复用引理）与 .mbt（可执行代码、契约、局部 proof_assert）两层；工作流为先定抽象模型、再定义最小不变量、用命名前后置谓词写契约、实现运行时代码、为每个与证明相关的循环加 proof_invariant、按需加 proof_assert 与辅助引理、由构造器向外缩小受信任桥。
使用方式：递归代码用结构化证明形状并加 proof_decrease；打包或索引表示先证具体更新事实再连到语义模型；循环产出值语义重要时用 proof_yield；共享 proof shim 保持最小；受信任桥视为临时手段。
调试与验证：证明失败后运行 moon prove <pkg>，查看 _build/verif/<pkg>/<pkg>.proof.json，先分类是算术/索引事实缺失、语义桥缺失、量词实例化问题、新引理扰动求解器还是前端限制，再决定修复方式。每次改动后运行 moon check <pkg>、moon prove <pkg>，运行时代码有变时再跑 moon test <pkg>；改动共享证明层需重跑依赖包。
限制：资料未提供支持的 MoonBit 版本、Why3 配置要求、性能数据或平台信息；应避免在契约中重复内联大公式、无检查就堆引理、同时改抽象设计与求解器引导等反模式。