formal-methods-drift-guard

docs と Z3 model は missing policy を拒否する fail-close 契約を示す一方、コードは許可し、ログでも U1 の export 許可が確認されている。これは code-drift（実装 drift）であり、現時点では新しい model check は not-run。temporary fallback を許容するか fail-close 契約を維持するかをドメイン担当者に確認し、決定に応じてコードまたは仕様・model・CI の lock を更新する。