菜单
由 vc-checking-subagent 在 vc-checking round worktree 中检查 generated manual VC 是否语义可证，并输出与当前 source_goal_version 绑定的 proof group plan。
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
由 annotation-subagent 在 annotation-filling 后检查 annotation round worktree 中的 C annotation 和 case_lib spec declarations，判断是否可交给 main agent 执行 annotation-check-round。
由 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。
为单个验证 case 定义 controller、main agent、fixed phase subagents、controller-owned vc-proving-preparing container、JSON handoff files、case_lib、group-worker deterministic merge 和 final-check 的协作合同。
基于 SOC 职业分类
| name | vc-checking |
| description | 由 vc-checking-subagent 在 vc-checking round worktree 中检查 generated manual VC 是否语义可证，并输出与当前 source_goal_version 绑定的 proof group plan。 |
本 skill 固定由 vc-checking-subagent 使用。它只读 agent_input.json 和 vc-checking round worktree，判断当前 generated manual VC 是否语义可证，并输出 proof group plan。
spawn.fork_context == false、fork_turns == "none"、parent_context_allowed == false；不得依赖 main agent 聊天历史。
docs/vc-checking-guide.md：P |-- Q 分析流程、judgment、group plan 模板和 annotation/spec blocker 信号。docs/natural-language-analysis.md：自然语言证明分析 group 的规范化输出、blocked 规则和与 proof group plan 的连接。*_goal.v、*_proof_auto.v、*_proof_manual.v、*_goal_check.vcase_libsource_versionsource_goal_versionproblem_context 和 annotation_design_summary，用于理解题目语义和 annotation 设计，不需要读取 parent chat。写入 agent_report.json.agent_result.vc_checking.group_plan。计划必须绑定当前 source_goal_version，并列出：
proof_groupsgroup_idwitness_namesrepresentative_witnessnatural_language_analysis，建议包含每个 witness 的自然语言可证性分析和用于分组的 analysis groups；该字段是 vc-checking 的结构化辅助，不是 controller acceptance gatevc-checking 应先用自然语言分析每个 target VC 的证明思路，再用这些分析辅助分组。若某个 VC 在语义上无法证明，返回 blocked 并说明应回到 annotation/spec 的原因，不交给 vc-proving-preparing / group-worker 硬证。若 VC 语义可证但需要 helper、证明较难或 proof route 不确定，应输出 proof plan 并交给 group-worker，不得 blocked。controller 不因缺失 natural_language_analysis 字段拒绝本轮；基本流程仍以 group_plan.proof_groups、版本和 witness 覆盖为准。
group plan 必须遵守 agent_input.json.grouping_policy。默认策略是 bounded witness groups：每组最多放入 max_witnesses_per_group 个 witness；当 target witness 数超过该上限时必须拆成多个 group。分组参考自然语言 analysis group、proof pattern、helper family、loop/refinement phase 和依赖关系，manual witness order 只作为确定性 tie-breaker。不得为了减少 spawn 数把大量 witness 无约束塞进一个组。
同时写 agent_output.txt 作为 non-authoritative reuse note。第一行必须是 # Reuse Note，正文包含 Note kind: non-authoritative reuse note 和 This file is not acceptance evidence.。
vc-checking-subagent 的 blocked 只用于两类情况：
P 确实无法推出 Q，并且缺口必须回到 C annotation 或 case_lib spec 修正。以下情况不得 blocked，必须自行处理并输出 group plan：helper 尚未证明、proof route 不确定、diagnostics hint 缺失、annotation design summary 缺字段、某些 witness 较难、需要把多个相关 witness 在 group size 上限内放进同一 group 由 worker 顺序证明。输入版本失效写 stale。context compaction 只写 compact-error 事实；是否重试或最终 block 由 controller / main agent 判定。
main agent 调用 vc-checking-check-round，确认 source versions 匹配、target witness 集合与 cleaned *_proof_manual.v 完全一致、没有重复分配、dependency graph 无环，满足 controller grouping policy，且 group plan 不要求修改 generated files 或 witness statements。