What is seLe4n?
seLe4n is a microkernel built from the ground up in Lean 4. Every kernel
transition is an executable pure function. Every invariant is machine-checked
by the Lean type-checker — zero sorry, zero axiom. The entire proof surface
compiles to native code with no admitted proofs.
The project preserves seL4's capability-based security model while introducing
architectural improvements enabled by the Lean 4 proof framework:
Scheduling and real-time guarantees
- Composable performance objects — CPU time is a first-class kernel object.
SchedContext encapsulates budget, period, priority, deadline, and domain into a reusable scheduling context that threads bind to via capabilities. CBS (Constant Bandwidth Server) scheduling provides proven bandwidth isolation (cbs_bandwidth_bounded theorem)
- Passive servers — idle servers borrow the client's
SchedContext during IPC, consuming zero CPU when not serving. The donationChainAcyclic invariant prevents circular donation chains
- Budget-driven IPC timeouts — blocking operations are bounded by the caller's budget. On expiry, threads are spliced out of the endpoint queue and re-enqueued
- Priority Inheritance Protocol — transitive priority propagation with machine-checked deadlock freedom (
blockingAcyclic) and bounded chain depth. Prevents unbounded priority inversion
- Bounded latency theorem — machine-checked WCRT bound:
WCRT = D × L_max + N × (B + P), proven across 8 liveness modules covering budget monotonicity, replenishment timing, yield semantics, band exhaustion, and domain rotation
Data structures and IPC
- O(1) hash-based hot paths — all object stores, run queues, CNode slots, VSpace mappings, and IPC queues use formally verified Robin Hood hash tables with
distCorrect, noDupKeys, and probeChainDominant invariants
- Intrusive dual-queue IPC — per-thread back-pointers for O(1) enqueue, dequeue, and mid-queue removal
- Capability derivation tree linked through the slots — each slot holds its parent, first-child and sibling links (seL4's mapping database), proven to agree with the tree; slot transfer, revocation and descendant traversal walk the links
Security and verification
- N-domain information-flow — parameterized flow policies generalizing seL4's binary partition. 44-entry enforcement boundary with per-operation non-interference proofs (35-constructor
NonInterferenceStep inductive), and a bounded, fail-closed declassification audit trail with a capability-gated reader
- Composed proof layer —
proofLayerInvariantBundle composes 16 subsystem invariant bundles (scheduler core + CBS extensions, capability, IPC + IPC–scheduler coupling, lifecycle, service, VSpace, cross-subsystem, TLB consistency, notification-waiter consistency, TLB-shootdown pending/ack bounds, per-core TLB invalidation and I-cache coherence, and the declassification audit-log bound) into a single top-level obligation verified from boot through all operations
- Three-phase state architecture — builder phase with invariant witnesses flows to a frozen immutable representation with proven lookup equivalence. 24 frozen operations mirror the live API
- Complete operation set — all seL4 operations implemented with invariant preservation, through thread suspend/resume, priority management (setPriority/setMCPriority), and IPC-buffer configuration
- Service registry — kernel-level service registration and lookup through the serving endpoint, recorded on the endpoint itself (seLe4n extension, not in seL4); dependency policy is left, as in seL4, to a user-level service manager
Current state
| Attribute | Value |
|---|
| Version | 0.36.165 |
| Lean toolchain | v4.28.0 |
| Production Lean LoC | 530,284 across 485 files |
| Test Lean LoC | 87,418 across 70 test suites |
| Proved declarations | 19,686 theorem/lemma declarations (zero sorry/axiom) |
| Rust crates | 4 (sele4n-types, sele4n-abi, sele4n-sys, sele4n-hal) across 80 source files |
| Target hardware | Raspberry Pi 5 (BCM2712 / ARM Cortex-A76 / ARMv8-A) |
| Hardware binding | H3 COMPLETE (WS-AG AG1–AG10): HAL, GIC-400, timer, ARMv8 page tables, FFI bridge, QEMU boot |
| Canonical audit | AUDIT_v0.29.0_COMPREHENSIVE — pre-1.0 comprehensive audit (202 findings; remediated by WS-AK AK1–AK10; archived) |
| Latest audit | AUDIT_v0.30.11_COMPREHENSIVE + AUDIT_v0.30.11_DEEP_VERIFICATION — pre-1.0 readiness audit cut after WS-AN closure (succeeds the now-archived AUDIT_v0.30.6_COMPREHENSIVE remediated by WS-AN AN0–AN12). WS-RC R0..R5 LANDED at v0.31.2; WS-RC R6..R14 absorbed into WS-SM per the SM0.Q.1 absorption mapping (see AUDIT_v0.30.11_WORKSTREAM_PLAN.md §15). Active workstream plan: . |
Metrics are derived from the codebase by ./scripts/generate_codebase_map.py
and stored in docs/codebase_map.json under the
readme_sync key. Update all documentation together with
./scripts/sync_documentation_metrics.sh (verify-only: --check);
./scripts/report_current_state.py remains a manual cross-check.
Quick start
./scripts/setup_lean_env.sh # install Lean toolchain
lake build # compile all modules
lake exe sele4n # run trace harness
./scripts/test_smoke.sh # validate (hygiene + build + trace + negative-state)
Documentation
docs/codebase_map.json is the source of truth for
project metrics. It feeds seLe4n.org
and is auto-refreshed on merge via CI. Regenerate with
./scripts/generate_codebase_map.py --pretty.
Validation commands
./scripts/test_fast.sh # Tier 0+1: hygiene + build
./scripts/test_smoke.sh # + Tier 2: trace + negative-state
./scripts/test_full.sh # + Tier 3: invariant surface anchors + Lean #check
NIGHTLY_ENABLE_EXPERIMENTAL=1 ./scripts/test_nightly.sh # + Tier 4: nightly determinism
./scripts/test_rust.sh # host Rust: build, tests, fmt, clippy
./scripts/test_aarch64_cross_build.sh # the kernel HAL's real target
Run at least test_smoke.sh before any PR. Run test_full.sh when changing
theorems, invariants, or Tier 3 anchors.
After any change under rust/, run both Rust lanes. They cover disjoint
halves of the same crate: on the host every #[cfg(target_arch = "aarch64")]
block is removed before rustc or clippy sees it, so the host lane cannot see
the 67 cfg-gated blocks, 57 asm! sites or four .S sources that make up
most of the HAL. The cross lane builds sele4n-hal for
aarch64-unknown-none-softfloat in both profiles, verifies the assembly
sources really assembled, lints the cross target, and disassembles the release
objects to prove they use no FP/SIMD register — the kernel is FP-free and traps
FP/SIMD at EL1 from its first instruction — and it is a build rather than a
cargo check, because check stops before code generation and never reaches
an assembler.
Architecture
seLe4n is organized as layered contracts, each with executable transitions and
machine-checked invariant preservation proofs:
┌──────────────────────────────────────────────────────────────────────┐
│ Kernel API (SeLe4n/Kernel/API.lean) │
├──────────────┬─────────────┬────────────┬───────────┬────────────────┤
│ Scheduler │ Capability │ IPC │ Lifecycle │ Service (ext) │
│ RunQueue │ CSpace/CDT │ DualQueue │ Retype │ Orchestration │
│ SchedContext │ │ Donation │ │ │
├──────────────┴─────────────┴────────────┴───────────┴────────────────┤
│ Information Flow (Policy, Projection, Enforcement) │
├──────────────────────────────────────────────────────────────────────┤
│ Architecture (VSpace, VSpaceBackend, Adapter, Assumptions) │
├──────────────────────────────────────────────────────────────────────┤
│ Model (Object, State, CDT) │
├──────────────────────────────────────────────────────────────────────┤
│ Foundations (Prelude, Machine, MachineConfig) │
├──────────────────────────────────────────────────────────────────────┤
│ Platform (Contract, Sim, RPi5) ← production bindings │
└──────────────────────────────────────────────────────────────────────┘
Source layout
SeLe4n/
├── Prelude.lean Typed identifiers, KernelM monad
├── Machine.lean Register file, memory, timer
├── Model/ Object types, SystemState, builder/freeze phases
├── Kernel/
│ ├── API.lean Unified public API + apiInvariantBundle
│ ├── Scheduler/ RunQueue, EDF selection, PriorityInheritance, Liveness (WCRT)
│ ├── Capability/ CSpace ops + CDT tracking, authority/preservation proofs
│ ├── IPC/ Dual-queue endpoints, donation, timeouts, structural invariants
│ ├── Lifecycle/ Object retype, thread suspend/resume
│ ├── Service/ Service registry and its invariants
│ ├── Architecture/ VSpace (W^X), TLB model, register/syscall decode
│ ├── InformationFlow/ N-domain policy, projection, enforcement, NI proofs
│ ├── RobinHood/ Verified Robin Hood hash table (RHTable/RHSet)
│ ├── RadixTree/ CNode radix tree (O(1) flat array)
│ ├── SchedContext/ CBS budget engine, replenishment queue, priority management
│ ├── FrozenOps/ Frozen-state operations + commutativity proofs
│ └── CrossSubsystem.lean Cross-subsystem invariant composition
├── Platform/
│ ├── Contract.lean PlatformBinding typeclass + BootVSpaceRootEntry
│ ├── Boot.lean Boot sequence (PlatformConfig → IntermediateState).
│ │ installBootVSpaceRoot threads canonical boot VSpace
│ │ through bootFromPlatformChecked (WS-RC R3).
│ ├── Sim/ Simulation platform (permissive contracts for testing)
│ └── RPi5/ Raspberry Pi 5 (BCM2712, GIC-400, MMIO).
│ VSpaceBoot.lean holds the canonical W^X-compliant
│ boot VSpaceRoot (production-wired since WS-RC R3).
├── Testing/ Test harness, state builder, invariant checks
Main.lean Executable entry point
tests/ Executable test suites + fixtures
Each subsystem follows the Operations/Invariant split: transitions in
Operations.lean, proofs in Invariant.lean. The unified apiInvariantBundle
aggregates all subsystem invariants into a single proof obligation. For the full
per-file inventory, see docs/codebase_map.json.
Comparison with seL4
| Feature | seL4 | seLe4n |
|---|
| Scheduling | C-implemented sporadic server (MCS) | CBS with machine-checked cbs_bandwidth_bounded theorem; SchedContext as capability-controlled kernel object |
| Passive servers | SchedContext donation via C | Verified donation with donationChainAcyclic invariant |
| IPC | Single linked-list endpoint queue | Intrusive dual-queue with O(1) mid-queue removal; budget-driven timeouts |
| Information flow | Binary high/low partition | N-domain configurable policy with a 44-entry enforcement boundary (count pinned by enforcementBoundaryExtended_count), per-operation NI proofs, and a capability-gated audit trail for every authorized declassification |
| Priority inheritance | C-implemented PIP (MCS branch) | Machine-checked transitive PIP with deadlock freedom and parametric WCRT bound |
| Bounded latency | No formal WCRT bound | WCRT = D × L_max + N × (B + P) proven across 8 liveness modules |
| Object stores | Linked lists and arrays | Verified Robin Hood hash tables (RHTable/RHSet) with O(1) hot paths |
| Service management | Not in kernel | Endpoint-backed service registry; dependency policy in user space |
| Proofs | Isabelle/HOL, post-hoc | Lean 4 type-checker, co-located with transitions — zero sorry/axiom (proved-declaration count in the Current state table) |
| Platform | C-level HAL | PlatformBinding typeclass with typed boundary contracts |
License and third-party attributions
seLe4n itself is licensed under the GNU General Public License v3.0 or later
(GPLv3+); see LICENSE for the full text. Third-party build
dependencies (cc, find-msvc-tools, shlex, all dual-licensed
MIT OR Apache-2.0) are used under the MIT option; their upstream copyright
and permission notices are reproduced verbatim in
THIRD_PARTY_LICENSES.md. No runtime-linked
third-party code is present in the kernel binary — the HAL is #![no_std]
and uses only core::*.
