规格与实现

这一章接在「规格接口」之后，继续回答一个更工程化的问题：

我们写下来的规格，怎样真正约束一段候选业务逻辑？

前一章已经把 Oxpecker 的库接口、规格文件、候选实现和检查入口拆开。这里会继续沿着 agent task 示例推进，重点讲清楚：

规格不是实现
状态映射
动作适配
实现一致性
反例如何回到业务代码
coding agent 修改实现时，规格怎样提供额外检查

这一章的目标不是增加很多新理论，而是让读者第一次完整看到：formal verification 不是只检查一个玩具模型，而是可以用规格约束候选实现，并把反例反馈到真实工程判断里。