seLe4n Simulator

Watch the kernel run — and the proofs hold

Every seLe4n transition is a deterministic pure function whose invariants are machine-checked by Lean. Step through a real execution trace below and watch threads move between the CPU, the run queue, and IPC wait queues — with the proven invariants holding at every step.

When sourced from a verified kernel export, every step is a faithful replay of a machine-checked run. The bundled sample is a hand-authored reference fixture that conforms to the same schema.