用途：对 LaTeX 数学证明做系统性验证与修复。读取证明后，借助外部评审后端（默认 Codex MCP，模型 gpt-6-astra，推理强度 ultra）进行跨模型对抗式评审，识别漏洞、修复、再评审，最多 3 轮，最终产出审计报告与证明义务核算。
主要能力：按 20 类问题分类（逻辑与证明结构、分析与测度论、模型与参数追踪、范围与声明）检查；采用双轴严重度（证明状态 × 影响）派生 FATAL/CRITICAL/MAJOR/MINOR 标签；建立依赖 DAG、假设台账、类型化符号表、规范量化陈述、微声明清单与极限顺序图；对 DCT、MCT、Fubini、Leibniz、隐函数定理等常见定理附条件清单；可选调用 /lean-formalize 做 Lean 形式化验证。
使用方式：在论文目录下调用，上下文经 $ARGUMENTS 传入。默认后端 codex，可用 --reviewer: oracle-pro 或 --reviewer: manual 覆盖；manual 后端不可用时须停止并打印安装命令，不得回退 Codex。评审调用约定：codex 用 mcp__codex__codex 新建线程、mcp__codex__codex-reply 续接；manual 用 mcp__manual_review__review 与 review_reply。产出 PROOF_AUDIT.md、proof_audit_report.tex、PROOF_CHECK_STATE.json、PROOF_SKELETON.md，默认经 /render-html 渲染 HTML。
限制：不得用 /loop、/schedule 或 CronCreate 包裹，因其带裁决性且依赖跨轮评审记忆；评审模型必须为非 Claude 模型，否则违反跨模型不变式；评审者一致或未找到反例不等于证明义务已解除。具体收费、平台支持等资料暂未提供。