This proof defines and proves the global invariants of seL4's abstract specification. The invariants are phrased and proved using a monadic Hoare logic described in a TPHOLS '08 paper.
To build from the l4v/ directory, run:
./isabelle/bin/isabelle build -d . -v -b AInvs
The top-level theory where the invariants are proved over the kernel is
Syscall_AI; the bottom-level theory where they are
defined is Invariants_AI.