工程集成

这里把 Oxpecker 放回真实软件开发工作流。

前面的章节已经让读者学会用 Zig 表达模型、性质、状态探索和反例反馈。这里要回答的是：这些能力怎样进入 coding agent、代码审查、CI、回归测试和长期规格维护，而不是只停留在本地练习。

计划覆盖：

coding agent 修改代码时怎样同步更新规格
怎样把模型检查作为回归验证的一部分
怎样用反例 trace 辅助 code review
怎样为系统模块维护小模型
怎样把规格、测试和实现放进同一个工程循环
怎样判断一个问题应该继续用 Oxpecker，还是引入成熟工具

成熟工具的参考不会消失，但它们会穿插在具体问题中出现：当某个模型表达、状态规模或证明需求超出 Zig-first 实践边界时，再讨论 TLA+、Alloy、SMT、Kani、Verus 或 Lean 能提供什么。