Formal Proofs about seL4

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 Proof
asmrefine - Assembly Refinement Proof
bisim - Bisimilarity of seL4 with a static Separation Kernel
capDL-api - CapDL API Proofs
crefine - C Refinement Proof
drefine - CapDL Refinement Proof
infoflow - Confidentiality Proof
invariant-abstract - Abstract Spec Invariant Proof
refine - Design Spec Refinement Proof
sep-capDL - CapDL Separation Logic Proof