This directory contains the formal proofs about seL4, which mostly prove properties about the various seL4 specifications.
Each such proof lives in its own subdirectory:
access-control- Access Control Proofasmrefine- Assembly Refinement Proofbisim- Bisimilarity of seL4 with a static Separation KernelcapDL-api- CapDL API Proofscrefine- C Refinement Proofdrefine- CapDL Refinement Proofinfoflow- Confidentiality Proofinvariant-abstract- Abstract Spec Invariant Proofrefine- Design Spec Refinement Proofsep-capDL- CapDL Separation Logic Proof