README.md
1Separation Kernel Bisimilarity
2==============================
3
4This proof establishes that seL4, if configured fully statically with 1-level
5CSpaces and notification caps only, is bi-similar to a static separation
6kernel that has no other system calls than signalling notifications.
7
8Building
9--------
10
11To build from the `l4v/` directory, run:
12
13 ./isabelle/bin/isabelle build -d . -v -b Bisim
14
15Important Theories
16------------------
17
18Theory [`Separation`](Separation.thy) defines static configurations, and
19theory [`Syscall_S`](Syscall_S.thy) contains the proof that this is equivalent
20to a static kernel.
21
22The definition of a static kernel API can be found in the `spec` directory
23under [`sep-abstract`](../../spec/sep-abstract/).
24