QualifiedCProgramming AGENTS.md

仓库定位

本仓库验证 C 程序：补充 annotation、运行 symbolic execution、检查 manual VC、证明 Rocq obligations，并完成最终一致性检查。

系统由 controller、main agent、每个 run 唯一且持续复用的 annotation-subagent、按轮创建的 vc-checking-subagent、controller-owned vc-proving-preparing、group-worker、机械 merge 和 final-check 组成。正式 C、generated files 与 Rocq formal files 始终以仓库根目录为当前状态；phase 不创建 Git 隔离目录。

外界只调用 .agents/skills/verification-orchestrator/scripts/controller.py。agent 不直接执行 controller 内部模块；controller handoff 提供完整的 symexec、coq-check、coq-debug 命令。

简化文件原则

• 给 agent 阅读的交接使用 Markdown；JSON 只保存 controller 必须解析的状态、terminal result、plan、manifest 与 merge result。
• 同一事实只记录一次。可由 controller state、固定目录或文件内容推导的信息，不复制进 report/manifest。
• JSON 不保存整份规则、parent transcript、完整 manifest 副本、预填 evidence、命令 argv/cwd/flags 副本或 state snapshot。
• 成功 evidence 只保存 status、版本与必要摘要；失败时保留首个 diagnostic 或 blocker。完整检查可通过同一 controller 命令重跑。
• final-check cleanup 只记录删除数量；失败只记录错误数、残留数以及首个错误或残留路径，不保存整份副产物路径列表。
• controller_state.json 是 current authority；agent report 只属于 owner，controller acceptance 写入 state/log，不反写 report。
• run_logs.json 是 append-only JSONL，只含事件，不重复整个 state。
• 所有机器读取的 JSON 都含 schema_version。Markdown 不使用伪 schema。
• agent_output.md / group_worker_output.md 用于简短的人类分析与 retry 参考，不是 acceptance evidence；没有固定套话模板。每次 annotation attempt 的 input/report/output 从创建起就位于独立 report directory，不覆盖前次文件；formal before/after 另存 run root history。

Skill routing

• verification-orchestrator：main agent 使用；控制单个 run、唯一 annotation 会话、round、group、merge、stale 与 final-check。
• annotation-filling：run 内唯一的 annotation-subagent 使用；首次读取相关示例并修改 main root target C annotation 与 formal_case_lib spec，后续接收 append feedback 继续修正。
• annotation-checking：唯一 annotation owner 的当前 turn 内使用；判断 candidate 是否可交 main-owned check。
• vc-checking：vc-checking-subagent 使用；只读 current formal files，输出 group plan。
• group-worker-proving：group-worker 使用；只证明 assigned witnesses，只改 group copies。
• final-check：main agent 使用；accepted merge 写回后检查 freshness、Coq、结构、三级 lib 与 cleanup。