Formal Verification Gates for AI Coding Loops