seLe4n Simulator
What the kernel does, how it checks, and why it is safe
Step through a scenario. Each step shows the state change, the checked syscall path that allowed or refused it, and the security properties and invariants it relies on, each linked to the Lean declaration that states or proves it.
The kernel does not export traces yet, so the scenarios are written by hand. Every function, theorem, invariant, right and error they name is the kernel's own: the build resolves each one in the seLe4n source at the commit above and fails if one is missing or misstated.
Kernel state
Security guarantees
Kernel invariants
Each invariant is a Lean predicate over the whole kernel state. A preservation theorem proves that a transition which starts in a state satisfying it ends in one that does too. Runtime checks are the test harness's executable mirrors of the same predicates; they test, they do not prove.