What is seLe4n?
seLe4n is a capability-based microkernel whose kernel model is written entirely in Lean 4 with machine-checked proofs, complemented by safe Rust syscall wrappers for user-space programs. It targets the Raspberry Pi 5 (ARM64 / BCM2712) as its first hardware platform.
Why a Microkernel?
Microkernels minimize the trusted computing base by running only essential services in kernel space — scheduling, IPC, capability management, and memory control. Everything else (drivers, filesystems, networking) runs in user space. This reduces attack surface and makes formal verification tractable: every line of kernel code can be reasoned about mathematically.
Why Lean 4?
Lean 4 is both a general-purpose programming language and an interactive theorem prover. seLe4n leverages this duality: the kernel is executable code whose properties are machine-checked at compile time. There is no separate specification language, no trusted translation step, and no semantic gap between the model and the running code. If it compiles, the proofs hold.
How It Works: Build → Freeze → Execute
seLe4n employs a three-phase architecture. During the Build phase, an IntermediateState wrapping SystemState with invariant witnesses is constructed through pure builder operations (createObject, insertCap, mapPage, registerIrq, registerService). Each builder operation preserves four structural invariants. During the Freeze phase, the one-way freeze function converts the builder state into a FrozenSystemState where all RHTable fields become FrozenMap structures (hash → index + contiguous array) and CNode slots become CNodeRadix flat radix arrays with zero-hash O(1) lookup. During the Execute phase, the frozen state serves value-only mutations for 20 of the kernel’s 30 syscalls — structural builder-phase operations and live-scheduler/cache-maintenance operations are served outside the frozen path — the index map is never modified, all Fin accesses are within bounds by construction, and no fuel or dynamic resizing is needed.
All three phases are unified by the KernelM monad, defined as σ → Except ε (α × σ) — a state-transformer with explicit error handling. The freeze step carries machine-checked lookup-equivalence proofs — every key readable in the builder state reads identically in the frozen state — and a commutativity layer establishes frozen_op(freeze(s)) = freeze(builder_op(s)) for value-only mutations, ensuring the frozen execution phase is semantically equivalent to the builder phase. Every transition is deterministic: given the same input state and system call, you always get the same output state.
What Makes It Different?
seLe4n unifies implementation and proof in a single language —
no separate proof assistant, no translation layer, no semantic gap. Each subsystem
follows an Operations/Invariant split: executable transitions live in
Operations.lean, and their machine-checked proofs live alongside in
Invariant.lean. The type-checker enforces that every invariant holds
across every operation.
Project Status
seLe4n is an active research project at version 0.33.100. The kernel
model is feature-complete with 30 syscalls spanning IPC, scheduling, capabilities, memory management,
notifications, information-flow control, and service orchestration.
A companion Rust workspace
provides safe, no_std wrappers for the kernel's syscall ABI.
The hardware binding for the Raspberry Pi 5 is complete — HAL, GIC-400 interrupt controller,
ARM Generic Timer, ARMv8 page tables, and QEMU boot — with SMP multi-core support as the
active workstream.
Created thoughtfully with the help of Claude and Codex.
Architecture
seLe4n follows a layered contract model.
Each subsystem's invariant proofs compose upward into a unified
apiInvariantBundle that covers the entire kernel.
A companion Rust workspace provides safe, no_std syscall wrappers above the API surface.
Prelude & Machine
Typed identifiers (ObjId, ThreadId, DomainId, Priority, CPtr, Slot, ASID, VAddr, PAddr, CdtNodeId, RegName, etc.) each with Hashable + LawfulHashable instances. The KernelM monad, register files, memory regions, and timer configuration. Sentinel value 0 reserved for ObjId, ThreadId, ServiceId, and CPtr with identity theorems.
Object Model & State
8 composable kernel object types: TCB, Endpoint,
Notification, CNode,
VSpaceRoot, Untyped,
SchedContext, Reply.
424 theorems across Object (204) and State (220).
Objects compose through typed Capability references with bitmask
AccessRightSet.
The SystemState record aggregates all stores into a single
immutable snapshot — backed by the verified RHTable for O(1) access everywhere.
Scheduler
1,723 theorems across 46 files spanning core operations, per-core SMP dispatch, priority inheritance, and liveness proofs. RunQueue backed by RHTable Priority (List ThreadId) with RHSet ThreadId membership index. Priority + EDF scheduling with domain-aware partitioning. schedulerWellFormed structural invariant. Operations split into Core, Preservation, and Selection. O(1) insert, remove, contains, and priority-bucketed candidate selection. PriorityInheritance with blocking graph analysis and bounded inversion. Liveness proofs including WCRT bounds and domain-rotation guarantees.
Capability & CDT
244 theorems across 12 modules. CNode slots backed by a verified UniqueSlotMap Capability for O(1) operations. Node-stable Capability Derivation Tree with childMap : RHTable CdtNodeId (List CdtNodeId). Invariant proofs split into Authority (24 theorems), Defs (62 theorems), and a six-file Preservation suite (105 theorems). Strict revocation via cspaceRevokeCdtStrict.
IPC & Dual-Queue
Deeply modularized across 52 files with 1,659 theorems. Intrusive dual-queue endpoints split into Core, Transport, and WithCaps. 517 structural invariant proofs, 39 endpoint preservation theorems, and 26 capability transfer proofs. Operations decomposed into CapTransfer, Endpoint, SchedulerLemmas, Donation, and Timeout.
Robin Hood Hash Map
Verified Robin Hood hash table implementation with 186 theorems across 8 modules. RHTable provides O(1) amortized insert, lookup, and erase with open addressing and linear probing. 46 bridge theorems connect the implementation to HashMap-compatible semantics. 64 preservation proofs and 44 lookup correctness theorems. Imported by Model.Object.Types — the verified foundation for all kernel hash-based data structures.
Information Flow
801 theorems across 14 deeply modularized files. Enforcement split into
Soundness and
Wrappers.
Invariant proofs decomposed into
Composition,
Helpers, and
Operations.
80 non-interference theorems spanning single-core, per-core, and cross-core proofs,
with proven reflexivity and transitivity.
Service Orchestration
120 theorems across 7 files. Graph-based dependency tracking with O(n+e) DFS cycle detection. Operations handles dependency management, Interface defines service contracts, and Registry manages service registration with its own invariants. Invariant proofs split into Acyclicity and Policy enforcement. Runtime lifecycle state is managed through the capability-indexed service registry.
Platform Layer
PlatformBinding typeclass defines runtime, boot, and interrupt
boundary contracts. BootBoundaryContract captures
per-platform boot guarantees. Concrete bindings for a simulator and the Raspberry Pi 5
(BCM2712 memory map, GIC-400 constants, ARM64 config, 48-bit VA / 44-bit PA).
Rust Syscall Wrappers
Four no_std Rust crates: three user-space crates provide ergonomic, fully safe, typed wrappers over the verified 30-syscall seLe4n ABI, while the kernel-side sele4n-hal supplies the ARM64 hardware abstraction layer. sele4n-types defines a 30-variant SyscallId enum, 16 #[repr(transparent)] newtype identifiers, a 55-variant KernelError enum (54 mirroring the Lean inductive plus a Rust-only forward-compatibility sentinel), and bitmask-based AccessRights — all with #![deny(unsafe_code)]. sele4n-abi handles ARM64 register encoding/decoding, IPC buffer overflow, and MessageInfo bitfield packing — with exactly one unsafe block: the inline svc #0 instruction in trap.rs. sele4n-sys exposes typed wrappers for IPC (send/receive/call/reply/replyRecv), CSpace (mint/copy/move/delete), lifecycle (retype), VSpace (map/unmap with W^X enforcement), service registry (register/revoke/query), TCB management (suspend/resume/setPriority), and notification (signal/wait) — zero unsafe code.
seLe4n vs Traditional Verified Kernels
seLe4n builds on decades of capability-based microkernel research while introducing architectural improvements enabled by the Lean 4 proof framework.
| Domain | Traditional | seLe4n |
|---|---|---|
| Language | C + assembly; proofs in Isabelle/HOL | Lean 4 for both implementation and proofs |
| Verification gap | Separate spec → C refinement chain | Zero gap — proofs live alongside code |
| Data structures | Linked lists, sequential lookups | Verified Robin Hood hash map — O(1) hot paths, 186 proofs |
| IPC queuing | Intrusive singly-linked list | Dual-queue (sendQ/receiveQ) with O(1) mid-queue removal |
| Scheduling | Priority-based round-robin | Priority + EDF with domain-aware partitioning |
| CDT | Mutable doubly-linked list | Node-stable with verified RHTable childMap, O(1) slot transfer |
| Information flow | Binary high/low partition | N-domain two-dimensional labels with per-endpoint policies |
| Service management | No kernel-level concept | Dependency graph with DFS cycle detection |
| Revocation | Silent error handling | Strict variant reporting first failure with context |
| Syscall boundary | Unverified register parsing | Verified decode with roundtrip + determinism proofs |
| User-space bindings | C headers with manual register marshalling | Safe Rust wrappers — 30 syscalls, typed capabilities, zero unsafe in sele4n-sys |
| State model | Mutable C structures | Immutable records, pure functional transitions |
| Object composition | Static object tables, manual pointer management | Composable typed capabilities with bitmask rights, 424 structural theorems |
| Execution model | Direct mutable state manipulation | Three-phase Build → Freeze → Execute with FrozenMap + CNodeRadix |
Key Innovations
seLe4n introduces architectural improvements across every subsystem, with O(1) data structures and machine-checked correctness at every layer.
O(1) Everywhere
Every hot-path data structure uses hash-based collections backed by a verified Robin Hood hash map with 186 theorems: object stores, run queues, CNode slots, VSpace mappings, IPC queues, ASID tables, CDT child lookups, notification waiters, and service dependency graphs. At freeze time, these become FrozenMap and CNodeRadix structures for deterministic O(1) access. Typed identifiers have Hashable + LawfulHashable instances. 400+ theorems re-verified after the data structure migration.
Verified Robin Hood Hash Map
Traditional verified kernels rely on linked lists with O(n) traversal. seLe4n builds on a ground-up verified Robin Hood hash table — 186 theorems across 8 modules, with 46 bridge theorems connecting the implementation to HashMap-compatible semantics. This is the verified algebraic foundation for every kernel data structure.
Priority-Bucketed Scheduler
Where traditional kernels use priority-based round-robin, seLe4n combines Priority + EDF with domain-aware partitioning. The RunQueue uses RHTable-backed priority buckets, reducing candidate selection from O(t) total threads to O(k) priority levels. The schedulerWellFormed structural invariant rolls into schedulerInvariantBundle, machine-checked across all 1,723 scheduler theorems, including priority inheritance and liveness proofs with WCRT bounds.
Intrusive Dual-Queue IPC
Traditional kernels use intrusive singly-linked lists for IPC queuing.
seLe4n endpoints maintain separate
sendQ/receiveQ with intrusive links for O(1) mid-queue removal.
WithCaps adds verified capability transfer across IPC boundaries —
1,659 theorems including
call-reply-recv composition proofs.
Capability Derivation Tree
Traditional kernels use mutable doubly-linked lists for capability tracking. seLe4n uses a node-stable CDT with RHTable-backed childMap for O(1) slot transfer. Unlike silent error handling in seL4, cspaceRevokeCdtStrict reports the first failure with full context. Bidirectional childMapConsistent invariant ensures the index stays synchronized.
N-Domain Information Flow
Where traditional kernels use a binary high/low partition, seLe4n implements a parameterized N-domain framework with two-dimensional labels (confidentiality + integrity). DomainFlowPolicy supports arbitrary flow topologies with proven reflexivity and transitivity. 80 non-interference theorems, 13-field ObservableState projection, and precomputed HashSet-based observability for O(1) lookups.
Service Orchestration
Traditional microkernels have no kernel-level service concept. seLe4n introduces
first-class service orchestration with graph-based lifecycle, O(n+e) DFS cycle detection,
and dependency-aware startup/shutdown. Invariant proofs split into
Acyclicity and
Policy
enforcement — 120 theorems across the service subsystem.
Verified Hardware Boundary
Where traditional kernels leave register parsing unverified, seLe4n verifies
the hardware-software boundary end-to-end.
RegisterDecode (24 decode-layer proofs) and
SyscallArgDecode (59 proofs including 23 round-trips) ensure no data
is misinterpreted at the trap boundary.
TlbModel adds flush-consistency proofs for the memory subsystem.
Safe Rust Syscall Wrappers
Where traditional kernels expose C headers with manual register marshalling,
seLe4n provides four no_std Rust crates — three user-space crates with fully safe,
typed APIs over the verified 30-syscall ABI, plus the kernel-side sele4n-hal
(ARM64 hardware abstraction layer).
sele4n-sys
introduces phantom-typed Cap<Obj, Rts>
capabilities with compile-time rights tracking and W^X enforcement.
The three user-space crates have zero unsafe except the single svc #0
trap instruction in
sele4n-abi;
the HAL confines hardware access to scoped unsafe blocks.
Composable Invariant Bundles
Each subsystem proves its own invariant bundle. Bundles compose upward:
coreIpcInvariantBundle,
ipcSchedulerCouplingInvariantBundle,
lifecycleCompositionInvariantBundle, and
vspaceInvariantBundle all roll up into
proofLayerInvariantBundle, exposed as the unified
apiInvariantBundle. A base-case theorem proves the
bundle holds for the default (empty) state.
Composable Performance Objects
Where traditional kernels use static object tables with manual pointer management, seLe4n’s 8 kernel object types compose through typed Capability references with bitmask-based AccessRightSet. All stores in SystemState are backed by the verified RHTable for O(1) access, and the CapDerivationTree enables composable revocation across the entire object graph — 424 theorems total.
Security Model
Security is woven into every layer of seLe4n through formal information-flow control, capability-based access mediation, and a documented threat model.
Information Flow Control
seLe4n enforces information-flow security at the kernel level through 801 theorems
across 14 modules. The DomainFlowPolicy
framework provides security guarantees that go beyond traditional binary high/low models:
- 80 non-interference theorems — per-operation proofs over the 35-constructor
NonInterferenceStepinductive, including 25 cross-core NI theorems under SMP - 38 operations classified by enforcement level
- Per-endpoint flow policies for fine-grained overrides
- Legacy embedding theorem proves the generic system subsumes the original
Capability-Based Access
All resource access is mediated through capabilities stored in CNode slots. The capability derivation tree tracks all parent-child relationships:
- O(1) slot operations via verified
UniqueSlotMap-backed CNodes - Strict revocation with explicit error reporting and context
- Node-stable CDT with
childMapRHTable index - Slot-reuse safety checks preventing dangling capabilities
- Policy-checked wrappers:
endpointSendDualChecked,cspaceMintChecked,registerServiceChecked - Sentinel ID rejection at IPC boundaries prevents ghost queue entries
Threat Model & Security Boundaries
Protected Assets
- Formal semantics and proof artifacts
- Executable evidence (traces and tier scripts)
- Supply-chain bootstrap infrastructure
- Repository integrity and CI policy state
Threat Actors
- External attacker: Public repo access, dependency injection
- Upstream compromise: Altered installer delivery
- Accidental insider: Secret commits, stale docs
- Fork CI: Limited upload permissions
Security Controls
- Expanded
.gitignoresecret/artifact denylist - SHA-256 verified
elaninstaller downloads - Tier-3 anchor checks against CI workflow semantics
- Blocking CodeQL gate with Tier-0 workflow-policy checks
Verification & Testing
seLe4n employs a multi-tiered verification strategy combining Lean's type-checker with runtime testing, ensuring correctness from proof to execution.
Hygiene
Forbidden-marker scans ensure zero sorry and zero axiom
across all production code. Documentation link validation, sync checks, and
formatting enforcement. The first line of defense.
Build
Full Lean compilation across 570 parallel build jobs. All 8472 theorems are type-checked. Every invariant proof, every bridge lemma, every preservation theorem is verified by the Lean type-checker. If it compiles, the proofs hold.
./scripts/test_tier1_build.shRuntime
Trace sequence probes validate executable behavior against formal semantics. The negative-state suite tests malformed input rejection across IPC, capabilities, endpoints, and CSpace mutations. Determinism validation runs the trace executable twice and requires identical output. Information-flow runtime checks verify enforcement wrappers.
./scripts/test_tier2_negative.sh && ./scripts/test_tier2_trace.sh && ./scripts/test_tier2_determinism.shInvariant Surface
Anchors every named theorem and invariant to the proof surface. Verifies that all documented claims in the Claim & Evidence Index are backed by actual code. Ensures no proof regressions across refactoring. The full correctness gate for PRs.
./scripts/test_tier3_invariant_surface.shNightly
Scenario-seed replay from the canonical catalog, staged experimental candidate validation, and long-running invariant probes. An opt-in Tier 5 harness cross-checks the Lean oracle against the Rust oracle. Catches subtle regressions that slip through faster tiers.
./scripts/test_nightly.shTest Shortcuts
| Command | Tiers | Use Case |
|---|---|---|
./scripts/test_fast.sh | 0 + 1 | CI — hygiene and build only |
./scripts/test_smoke.sh | 0 + 1 + 2 | Minimum PR requirement |
./scripts/test_full.sh | 0 + 1 + 2 + 3 | Full verification — invariant/theorem changes |
./scripts/test_nightly.sh | 0 + 1 + 2 + 3 + 4 | Nightly CI — determinism + experimental |
Proof Quality Classification
High Assurance
- Substantive preservation
- Compositional preservation
- Structural invariants
- End-to-end chains
- Non-interference proofs
Low Assurance
- Error-case preservation
- Trivially true for unchanged state returns
Resolved Findings
- C-01: Tautological proofs → refactored
- H-01: Non-compositional proofs → refactored
- H-03: Badge safety gap → closed
API Surface
The kernel exposes a stable public API through SeLe4n/Kernel/API.lean
via the unified syscallEntry / syscallEntryChecked dispatch path.
All 30 syscall-facing operations are routed through capability-gated dispatch with information-flow enforcement.
The production entry point syscallEntryChecked enforces flow policies; the unchecked syscallEntry is retained for backward compatibility with existing proofs.
27 of the 30 syscalls have corresponding safe Rust wrappers in sele4n-sys.
Project Structure
285 Lean modules, 61 test and CI scripts, and 248 documentation files with specifications, ADRs, and roadmaps.
@[extern] hooks)Getting Started
Whether you want to explore the kernel model, contribute proofs, or understand the architecture — here is how to get up and running.
Clone the Repository
git clone https://github.com/hatter6822/seLe4n.git
cd seLe4nSet Up the Lean Environment
The setup script installs elan (the Lean version manager) with
SHA-256 checksum verification and the pinned Lean 4.28.0 toolchain.
./scripts/setup_lean_env.shBuild & Verify
Build the entire kernel. All 8472 theorems are checked during compilation
across 570 parallel build jobs. Zero sorry, zero axiom.
lake buildRun Tests
Start with the smoke test (minimum for PRs), then run the full suite for invariant work.
# Minimum PR requirement (Tiers 0-2)
./scripts/test_smoke.sh
# Full verification (Tiers 0-3)
./scripts/test_full.sh
# Quick CI check (Tiers 0-1 only)
./scripts/test_fast.shBuild Rust Syscall Wrappers
The rust/ workspace
provides safe, no_std wrappers around the seLe4n syscall surface (27 of the 30 syscalls). Builds on both ARM64 (real trap) and x86_64 (mock trap for host-based testing).
cd rust
cargo build
cargo testContributing
seLe4n welcomes contributors. Before submitting a PR:
- Read the Contributing Guide and Development Docs
- Identify which area of the project your change addresses
- Run
./scripts/test_smoke.shat minimum;test_full.shfor theorem changes - Update invariants and theorems together with code changes
- Keep PRs focused on one coherent unit of work
- State transitions must have explicit success or failure outcomes
Documentation
Comprehensive docs live in the docs/ directory:
- Master Specification — Complete kernel design
- Development Guide — Workflow and standards
- Testing Framework — Tier organization
- Threat Model — Security boundaries
- IF Roadmap — Non-interference proof status
- Claim & Evidence Index — Verification traceability
- Platform Binding ADR — Hardware abstraction design
- VSpace ADR — Memory model decisions
Roadmap
Development is organized into milestones covering kernel semantics, audit remediation, performance, and hardware binding. Here is where the project stands.
M1–M7: Semantic Foundations Complete
Scheduler semantics, capability/CSpace operations, IPC seeds, waiting handshake, lifecycle/retype, capability composition, service graphs, architecture boundary assumptions, and initial audit remediation.
Audit Portfolios Complete
Four complete audit portfolios: comprehensive audit, model/docs/maintainability, test validity and proof gaps, and test/CI and kernel hardening. All findings closed.
Critical Audit Remediation Complete
Intrusive dual-queue IPC with message transfer verification. Untyped memory retype with watermark tracking. Information-flow completeness — 13-field ObservableState projection. Proof gap closure across all operations.
Performance Optimization Complete
Migrated all hot paths to O(1) hash-based structures. 14 performance audit findings eliminated. Typed identifier Hashable instances, object store HashMap, ASID resolution table, RunQueue restructure, CNode slot HashMap, VSpace mapping HashMap, IPC dual-queue + notification, graph traversal optimization, and information-flow projection optimization. 400+ theorems re-verified.
Rust Syscall Wrappers Complete
Three no_std Rust crates (sele4n-types,
sele4n-abi,
sele4n-sys)
providing safe wrappers around all 25 syscalls of the surface as it stood at completion (the surface has since grown to 30, of which sele4n-sys wraps 27) including notification, compound IPC, scheduling contexts, and TCB management. Phantom-typed capabilities,
ARM64 register ABI layer, W^X enforcement, IPC buffer overflow handling.
Single unsafe block isolated to the svc #0 trap instruction.
Build → Freeze → Execute Pipeline Complete
Implemented the Build → Freeze → Execute pipeline with commutativity proofs for all 12 frozen operations establishing frozen-phase semantic equivalence. FrozenOps subsystem with typed lookups, value-only mutations, and queue operations — all with isolation and preservation proofs.
Syscall Surface Expansion Complete
Expanded from 14 to 25 syscalls: added notification (Signal/Wait), compound IPC (ReplyRecv), scheduling context (Configure/Bind/Unbind), and TCB management (Suspend/Resume/SetPriority/SetMCPriority/SetIPCBuffer). Unified syscallEntry / syscallEntryChecked dispatch path with capability-gated routing. Rust ABI hardening with the SyscallId enum (since grown to 30 variants).
Refinement Complete
Model fidelity — badge bitmask, per-thread registers, multi-level CSpace.
Invariant quality — tautology reclassification, adapter proof hooks.
Testing expansion — oracle, probe, and fixture coverage.
Cleanup — dead code removal, legacy/dual-queue resolution.
H3: Raspberry Pi 5 Platform Binding Complete
Hardware binding portfolio (WS-AG, AG1–AG10) delivered: the sele4n-hal bare-metal crate,
GIC-400 interrupt dispatch, ARM Generic Timer, ARMv8 page tables with ASID management,
exception and interrupt models, cache coherency and speculation barriers,
an FFI bridge with 17 @[extern] functions, and QEMU boot verification.
BCM2712 memory map with 48-bit VA / 44-bit PA address space.
WS-SM: SMP Multicore Completion In Progress
Per-core scheduler, IPC, and TLB-shootdown semantics. Verified lock primitives — ticket lock and RwLock with refinement bridges — with deadlock freedom and serializability proofs. Cross-core non-interference and per-core information-flow projection.
Target: v1.0.0 — a bootable verified SMP microkernel on all four Raspberry Pi 5 cores. Latest: SM8.B per-core non-interference landed in v0.33.5.
H4 & IF-M5: Evidence Convergence Planned
Proof-to-platform convergence. Map model observability assumptions to RPi5 adapter obligations. Document unresolved security debt for side-channel follow-up.