Restricted Zig Verification

Restricted Zig Verification moves Oxpecker from hand-written models toward checking small Zig programs.

The first target is not arbitrary Zig verification. It is a clearly bounded subset with explicit unsupported constructs.