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 for the ARM architecture from the l4v/ directory, run:
L4V_ARCH=ARM ./run_tests 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.