README.md
1Formal Proofs about seL4
2========================
3
4This directory contains the formal proofs about seL4, which mostly prove
5properties about the various seL4 [specifications](../spec/).
6
7Each such proof lives in its own subdirectory:
8
9 * [`access-control`](access-control/) - Access Control Proof
10 * [`asmrefine`](asmrefine/) - Assembly Refinement Proof
11 * [`bisim`](bisim/) - Bisimilarity of seL4 with a static Separation Kernel
12 * [`capDL-api`](capDL-api/) - CapDL API Proofs
13 * [`crefine`](crefine/) - C Refinement Proof
14 * [`drefine`](drefine/) - CapDL Refinement Proof
15 * [`infoflow`](infoflow/) - Confidentiality Proof
16 * [`invariant-abstract`](invariant-abstract/) - Abstract Spec Invariant Proof
17 * [`refine`](refine/) - Design Spec Refinement Proof
18 * [`sep-capDL`](sep-capDL/) - CapDL Separation Logic Proof
19
20