菜单
由 annotation-subagent 在 annotation-filling 后检查 annotation round worktree 中的 C annotation 和 case_lib spec declarations，判断是否可交给 main agent 执行 annotation-check-round。
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
由 annotation-subagent 在 annotation round worktree 中填写或修正 C annotation，并在同一正式相对路径的 case_lib 中维护数学 spec declarations；完成后交给 annotation-checking。
由 main agent 在 final-candidate-apply 后执行最终检查，确认 generated files、manual proofs、case_lib 和 main worktree 状态一致。
由 group-worker 使用，读取 group_worker_input.json，在 group worktree 中证明 assigned witness blocks，并只在 group-local case_lib 中新增带当前 group_id suffix 的 helper declarations 和必要 Rocq 官方库 import。
由 vc-checking-subagent 在 vc-checking round worktree 中检查 generated manual VC 是否语义可证，并输出与当前 source_goal_version 绑定的 proof group plan。
为单个验证 case 定义 controller、main agent、fixed phase subagents、controller-owned vc-proving-preparing container、JSON handoff files、case_lib、group-worker deterministic merge 和 final-check 的协作合同。
| name | annotation-checking |
| description | 由 annotation-subagent 在 annotation-filling 后检查 annotation round worktree 中的 C annotation 和 case_lib spec declarations，判断是否可交给 main agent 执行 annotation-check-round。 |
本 skill 是 annotation-subagent 的同 round 质量检查步骤。它只判断 candidate 是否值得交给 main agent 执行 annotation-check-round；它不写 acceptance。
docs/spec-quality-checklist.md：case_lib、函数规格、loop invariant、QCP evidence 和 generated VC 语义预检。case_lib 能由 main worktree 的 coq_tooling.py check --target-kind case_lib 加载；--workspace-root 必须是当前 annotation round worktree，--target-file 指向 Rocq formal case_lib。case_lib 不含 Admitted.、extra Axiom 或当前 case generated artifact 的 SimpleC.EE.* import。case_lib 中有 mathematical definition。canonical_symexec_evidence 来自当前 annotation round worktree，匹配当前 source_version，并记录可参数化 QCP driver、cwd、canonical -I 和 -slp。passed；只能在 qcp_mcp_interactive_evidence 中写 skipped、failed 或 forbidden。在 agent_result.annotation.annotation_checking 中写：
status: passed | failedcase_lib_coqc_statuscanonical_symexec_statusqcp_mcp_interactive_statusrework_plan[]annotation-checking 自身不把 spec 质量、annotation 不充分、case_lib 声明缺失或 QCP 诊断失败判成 terminal blocker；这些都应输出 failed + rework_plan[]，交给 annotation-filling 在同一 spawn 内继续修。只有 annotation-checking 所需必要工具完全不可运行且有 command evidence 时，才建议 annotation result 使用 blocked。输入版本失效应建议 stale，不是 blocked。context compaction 只写 compact-error 事实；是否重试或最终 block 由 controller / main agent 判定。