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.