当前状态

这页记录 Oxpecker 作为 AI 辅助开发验证工具链的当前状态。

它回答四个问题：

• 现在已经能用什么？
• 正在塑形什么能力？
• 哪些方向仍然只是研究？
• 它怎样降低 agent 生成代码带来的代码审查不确定性？

当前概览

现在

显式状态检查器雏形

最小 checker 已经能探索有限模型、检查不变量，并为状态逻辑输出反例 trace。

推进中

审查证据形态

下一步的压力点是把 checker 输出整理成人类审查者能直接使用的证据。

风险

错误信心

Oxpecker 不能暗示一次模型检查已经证明生成代码完全正确，除非模型、适配层和边界足以支持这个结论。

轨道状态

轨道	状态	当前重点
检查器核心	现在	稳定结果类型、trace 所有权和搜索限制
规格表达层	下一步	让生成代码旁边的规格更容易编写和审查
状态空间工程	下一步	高效 visited state 存储和状态增长诊断
性质系统	下一步	死锁检测和有界时序检查
符号方法	研究	约束导出和 solver-backed 实验
受限 Zig 验证	研究	定义一个很小、可检查的 Zig 子集
证明边界	稍后	小型 proof checker 和 proof obligation 示例
工具链集成	下一步	CLI、报告、CI、agent / 审查输出

更新规则

只有出现具体证据时，状态才应该更新：

• 有可运行的 Zig 示例；
• 有一组失败和通过的检查样例；
• 有可测试的结果类型或 CLI 行为；
• 有解释检查结果的审查 artifact；
• 或者有已经记录在代码和路线图里的设计决策。