Verification capabilities

These records describe specific, bounded connections between public Zig APIs, Lean claims, and executable evidence. They are not blanket verification badges.

Capabilities

• choir.cfg.predecessor-mirror — CFG predecessor consistency
  Lean proves selected CFG model invariants. A bounded Zig property exercises the related public block-mutation API.

Audit