ACCESS CONTROL, PROVEN, THEN BUILT

One identity holds every compartment it is granted, evaluated at every access. Non-interference is machine-checked in Lean; 23 differential gates pin every enforcement layer to the proof. What is not proven is disclosed as a frontier, not claimed.

mike@0pon.com  ·  Demo on request: one command, ten seconds to a browser