检查器核心

检查器核心是 Oxpecker 的基础。

目标是把当前显式状态检查器打磨成稳定、可嵌入的 Zig 库：它能探索有限模型、检查性质，并为 agent 修改过的状态逻辑返回可复现的反例 trace。

在 AI 辅助开发场景里，检查器核心负责把一次生成代码变更转化为审查证据。如果 agent 修改了取消、重试、队列、回调或生命周期逻辑，Oxpecker 应该能运行对应模型并回答：探索了哪些状态，哪个性质失败，以及哪一串事件能复现这个失败。

状态

现在已有种子实现；库语义还需要继续加固。

目标能力

• 稳定 Spec、Action、Invariant、CheckResult 和 TraceStep。
• 支持多个初始状态。
• 支持多个被检查性质。
• 搜索限制必须返回明确的 incomplete 结果。
• 动作顺序保持确定性。
• 精确相等性是状态身份的语义来源。
• hash 只能作为优化，命中后仍需相等性确认。
• 结果元数据要服务代码审查：模型名、性质名、探索状态数、限制原因和 trace。

近期工作

1. 区分 holds、violated、deadlock、incomplete 等结果状态。
2. 为每个结果增加搜索统计。
3. 明确 trace 的内存分配和所有权。
4. 为重复状态、trace 重建和搜索限制增加测试。
5. 整理失败输出，让它不依赖 checker 内部知识也能贴进代码审查。

完成标准

• zig build test 覆盖成功、性质违反、重复状态处理和有界不完整搜索。
• 至少两个示例使用同一套公开 checker API。
• hash collision 不会隐藏两个语义上不同的状态。
• 审查者能根据报告中的 trace 复现一次失败的 agent 生成变更。