ACCESS CONTROL, PROVEN, THEN BUILT

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

Read the technical write-up  ·  mike@0pon.com  ·  Demo on request