工作区审计（2026-04-18）
- 状态：point-in-time audit（阶段性审计）
- 读者：维护者、贡献者
- 权威性：阶段性审计；从属于 QED 形式规范、当前代码/测试以及实现文档
- 范围：在审计基线上仍然重要的风险、缺口与后续事项
- 最后审阅：2026-04-18
日期：2026-04-18
本报告依据仓库的事实来源顺序，对当前工作区进行审计：
本次审计使用的验证基线：
moon test-> 通过（276/276）formal_verification/lake build-> 通过
这些全绿的闸门表明工作区在当前基线上是内部一致的，但并不意味着所有规划中的产品能力都已发布。
自上次审计以来已解决
以下先前报告的风险已不再是当前发现：
- 类型语言的可容许性现已在可信的定理 / 语句边界上强制执行；
- 联结词识别现已基于定义定理，而不再是单纯接受原始头部名称；
- 非
bool的表层联结词现已以结构化错误失败即关闭 (fail closed)，而不再在用户可达路径上崩溃。 - theorem-name inventory、
exact/applymode boundary，以及 canonical positive / negative script corpus 现在都已显式化并有回归覆盖。 - 以文件为先的
cmd界面现已存在，有回归测试覆盖，并使用结构化的策略 (tactic) 失败上下文，而不再只是原始字符串报告。 - 当前的 M4 切片现已集成到已发布路径上：定理头部绑定子、顺序块体定理脚本解析、原始的绑定子/目标/步骤跨度，以及结构化前端诊断均有回归覆盖。
ProofState的最终定理校验现已收紧为严格的规范化相继式匹配，并有回归测试拒绝旧的宽松匹配行为。- 析取包装 (disjunction wrap) 重放现已强制执行与合取合并相同的、显式的完整目标后置条件规范。
- 局部
exact见证现已仅冻结到活动假设别名，局部遮蔽不再回落到同名的定理条目。 - 规范的 prover 语料与映射矩阵覆盖现已与加固后的重放/最终定理契约对齐，因此
H5不再依赖过时的、更宽的语料契约。 - 最小化的
M4b现已在主定理脚本路径上发布：split/left/right的结构化分支块可被解析、重放，由 parser/prover/cmd 回归测试覆盖，并以稳定的分支路径给出诊断。
因此，本次审计只关注当前仍然重要的遗留问题和缺口。
发现
[P2] Lean 这条线仍是论文/符合性包，而不是对 MoonBit 实现的直接证明
为何重要
这不是 MoonBit 内核的缺陷，但它是诚实沟通时重要的状态边界。lake build 证明的是论文模型和抽象的符合性义务，并不会以机械方式把当前 MoonBit 源码树与 Lean 的 Realization 绑定起来。
证据
formal_verification/QEDFV/Engineering/Conformance.lean讨论的是抽象的实现 (realization) 与义务；- 可追溯性文件和规则映射文件是论文/符合性产物，而不是指向 MoonBit 符号的生成链接；
- 仓库文档已将 Lean 这条线视为论文优先，而非对实现的直接验证。
影响
- 对外的保证性表述必须保持精确；
lake build应理解为“规范/符合性包已闭合”，而不是“MoonBit 程序经机器检查与 Lean 等价”。
所需后续工作
- 在这一边界上保持文档精确；
- 仅当把具体的 MoonBit 到 Lean 的绑定方案作为新里程碑引入后，才增加更强的论断。
已开立的任务
A6
仍然重要的测试缺口
当前测试套件很强，但以下缺口对后续阶段仍然重要：
- 在当前最小分支块切片之外，更丰富的证明块展开；
- 在规范的未完成情形之外，更丰富的 hole / 未完成证明报告；
- 面向量词的前端及其与可信性相关的降级 (lowering) 契约；
- 任何未来的 CLI 功能都必须继续复用当前的正/负语料，而不是另起第二套脚本矩阵。
总体评估
- 内核以及当前产出定理的命题子集，所处状态明显强于上一次审计快照所描述的状态。
- 本次评审未在当前已发布路径上发现对已检查内核可靠性的直接破坏。
- 现在最重要的后续工作是：
- 让新的结构化分支块界面保持在同一个经检查的降级 (lowering) / 重放边界上；
- 让路线图转向更丰富的面向用户的证明体验：脚本、目标、证明块和量词前端；
- 随着前端扩展，持续维护语料、文档和符合性。
- rewrite/simplify 这条线仍然仅限研究。
- Lean 这条线保持全绿且有价值，但除非日后明确加入更强的实现绑定，否则应继续将其描述为论文/符合性包。