Auditing Soundness in Hand-Written Learned Access Control Shields

Formal verification of hard-deny shields in learned access control reveals high unsoundness rates between 0.50 and 0.70. When using prose-based restrictions, 97% of counterexamples are granted by other rules, potentially withholding 16-78% of intended policy permissions.