完成信号

Oxpecker 的路线图条目不会因为概念出现在文档里就算完成。只有工具行为真实存在，并且可以被检查，才算完成。

由于 Oxpecker 面向的是 AI 辅助开发中的验证瓶颈，完成还必须包含代码审查价值。一个能力不能只是本地能跑；它必须帮助人类审查者更清楚地判断一次 agent 生成或修改的代码是否可信。

必要证据

每个已完成能力都应该具备：

• 一个可运行的 Zig 示例；
• 一个能证明 checker 可以发现问题的失败样例；
• 一个能证明预期设计通过检查的成功样例；
• 一个能区分实际结果的结果类型；
• 一个可复现的命令；
• 足够支持代码审查的 trace 或报告输出；
• 对“这个结果没有证明什么”的明确说明。

结果边界

Oxpecker 应该把这些结果分开表达：

结果	含义
holds	在声明的边界内，已探索模型满足被检查的性质。
violated	某个可达状态或 trace 违反了性质。
deadlock	探索到某个可达状态，并且该状态在模型规则下没有任何合法下一步。
incomplete	checker 因为限制而停止，不能从中推断成功。
unsupported	请求的模型、语言结构或验证子集超出当前能力。

重新评估触发条件

出现下列情况时，需要重新修订路线图：

• Zig 到达 1.0 或重要 compiler / interface 稳定性里程碑；
• Oxpecker 开始消费 Zig compiler IR；
• 外部 solver 集成进入主线工具；
• 状态空间工程成为主要瓶颈；
• 外部用户开始在 CI 或代码审查中依赖 Oxpecker 结果；
• agent 生成代码成为主要集成目标；
• 任何结果描述有把有界验证夸大成无界证明的风险。