This proof establishes that seL4, if configured fully statically with 1-level CSpaces and notification caps only, is bi-similar to a static separation kernel that has no other system calls than signalling notifications.
To build from the l4v/ directory, run:
./isabelle/bin/isabelle build -d . -v -b Bisim
Theory Separation defines static configurations, and
theory Syscall_S contains the proof that this is equivalent
to a static kernel.
The definition of a static kernel API can be found in the spec directory
under sep-abstract.