受限 Zig 验证

受限 Zig 验证把 Oxpecker 从“执行用户写出的模型”推进到“检查一小段 Zig 程序”。

目标不是验证任意 Zig 程序，而是定义一个边界清楚、遇到不支持结构会明确失败的小子集。

这是通向 Oxpecker 核心问题的直接桥梁：FV 能否约束 agent 实际写出的代码，而不只是检查旁边手写的模型？诚实的起点不是完整 Zig 验证，而是一个很小的子集，让 Oxpecker 可以根据显式性质检查简单生成函数。

状态

研究依赖语言稳定性、compiler 访问方式和足够小的语义目标。

目标能力

• 纯函数子集。
• 有界整数。
• 第一版子集不包含 allocator。
• 第一版子集不包含 FFI。
• 第一版子集不包含并发。
• 源码级反例报告。
• 从模型级检查走向源码级检查的 adapter 路线。

近期工作

1. 定义第一版支持子集。
2. 决定消费 AST、IR，还是用户手写 adapter。
3. 为直线代码生成 path condition。
4. 对不支持结构明确报错。
5. 用同一个行为对比模型检查版本和受限源码检查版本。

完成标准

• 一个小 Zig 函数可以根据性质被检查。
• 不支持结构产生清楚错误。
• 结果解释被检查的子集和语义假设。
• 生成函数可以根据可审查的原因被接受、拒绝或标记为 unsupported。