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 the Lean kernel model 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 and no translation step between the Lean model and its executable code; the hardware boundary beneath it — the Rust HAL behind the FFI bridge's @[extern] functions — is a documented trusted contract. 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, frozen counterparts exist for the value-only mutations of 18 of the kernel’s 42 syscalls (pinned by frozenOpCoverage_count); structural builder-phase operations and live-scheduler/cache-maintenance operations have none. In the frozen state the index map is never modified, all Fin accesses are within bounds by construction, and no fuel or dynamic resizing is needed. The frozen phase is proved equivalent to the builder phase but is not yet the syscall dispatch path: API.lean still runs over the live state.
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.36.121. The kernel model is feature-complete with 42 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 — and the active workstreams are the bare-metal boot path (WS-BP) and a syscall path that allocates nothing (WS-ZA), as seL4's allocates nothing.
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, 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
1The SystemState record aggregates all stores into a single immutable snapshot — its object store a verified RHTable keyed by ObjId.
Scheduler
2,955 theorems across 64 files spanning core operations, per-core SMP dispatch, priority inheritance, and liveness proofs. Each core keeps only its run queue's ends (RunQueueEnds): the ends of the queue of runnable threads and of each priority bucket, and the highest queued priority. The links live in the TCBs, as seL4's tcbSchedNext/tcbSchedPrev, so insert, remove and membership are O(1) and selection starts at the highest queued bucket. Priority + EDF scheduling with domain-aware partitioning. schedulerWellFormed structural invariant. Operations split into Core, Preservation, and Selection. PriorityInheritance with blocking graph analysis and bounded inversion. Liveness proofs including WCRT bounds and domain-rotation guarantees.
Capability & CDT
353 theorems across 14 modules. A CNode's slots are a fixed array of 2radixWidth cells written in place, as seL4's cte_t array, and each slot holds its own derivation links (LinkField: parent, first child, next and previous sibling), so the slot is the derivation-tree node, as in seL4's mapping database — proven to agree with the ghost tree (cdtLinksAgree). Invariant proofs split into Authority (39 theorems), Defs (47 theorems), and a Preservation suite (104 theorems across 7 files). A delete splices its slot out of the tree (spliceNode), and cspaceRevokeCdtFinalising revokes as seL4's cteRevoke does: it deletes the source's first child until none is left.
IPC & Dual-Queue
Deeply modularized across 94 files with 4,493 theorems. Intrusive dual-queue endpoints split into Core, Transport, and WithCaps. 673 structural invariant proofs, 42 endpoint preservation theorems, and 31 capability transfer proofs. Operations decomposed into CapTransfer, Endpoint, SchedulerLemmas, Donation, and Timeout.
Robin Hood Hash Map
Verified Robin Hood hash table implementation with 259 theorems across 11 modules. RHTable provides O(1) amortized insert, lookup, and erase with open addressing and linear probing. 52 bridge theorems connect the implementation to HashMap-compatible semantics. 64 preservation proofs and 49 lookup correctness theorems. Imported by Model.Object.Types — the verified foundation for all kernel hash-based data structures.
Information Flow
1,526 theorems across 24 deeply modularized files. Enforcement split into
Soundness and
Wrappers.
Invariant proofs decomposed into
Composition,
Helpers, and
Operations.
A non-interference proof for each of the 35 kernel steps, 39 more for
cross-core operations, and proven reflexivity and transitivity.
Service Orchestration
118 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, QEMU's virt board (the kernel's first executed boot, on four PEs) and the Raspberry Pi 5 (BCM2712 memory map, GIC-400 constants, ARM64 config, 48-bit VA / 40-bit PA).
Rust Syscall Wrappers
Four no_std Rust crates: three user-space crates provide ergonomic, fully safe, typed wrappers over the whole verified 42-syscall seLe4n ABI, while the kernel-side sele4n-hal supplies the ARM64 hardware abstraction layer. sele4n-types defines a 42-variant SyscallId enum, 16 #[repr(transparent)] newtype identifiers, a 59-variant KernelError enum (58 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 operation: the inline svc #0 instruction in trap.rs. sele4n-sys exposes typed wrappers for IPC (send/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 | No spec-to-code gap in the Lean model — proofs live alongside code; the hardware boundary is a documented trusted contract |
| Data structures | Linked lists, sequential lookups | Verified Robin Hood tables for keyed maps (259 proofs); queues linked through the TCBs |
| IPC queuing | One queue per endpoint, its direction in the endpoint state | Separate send and receive queues linked through the TCBs, O(1) mid-queue removal |
| Scheduling | Priority-based round-robin | Priority + EDF with domain-aware partitioning |
| CDT | Mapping database linked through the slots | The same links in each slot, proven to agree with a ghost derivation tree |
| 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 | cteRevoke loop over the mapping database |
The same loop, checked before any write; a delete never refuses on derived capabilities |
| Syscall boundary | Unverified register parsing | Verified decode with roundtrip + determinism proofs |
| User-space bindings | C headers with manual register marshalling | Safe Rust wrappers — all 42 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, 1,059 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
Hot paths touch a constant number of words. The object store, VSpace mappings, ASID table, priority-bucket ends and service dependency graph are verified Robin Hood tables with 259 theorems; the kernel's queues — run queues, endpoint and notification queues, reply waiters — are linked through the TCBs, and a CNode's slots are a fixed array, as in seL4. At freeze time the tables become FrozenMap and CNodeRadix structures for deterministic O(1) access. Typed identifiers have Hashable + LawfulHashable instances.
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 — 259 theorems across 11 modules, with 52 bridge theorems connecting the implementation to HashMap-compatible semantics. It backs the object store and every keyed map the kernel keeps.
Priority-Bucketed Scheduler
Where traditional kernels use priority-based round-robin, seLe4n combines Priority + EDF with domain-aware partitioning. Each core's RunQueueEnds records the highest queued priority, so selection starts at the top bucket rather than scanning every thread, and the queue's links live in the TCBs. The schedulerWellFormed structural invariant rolls into schedulerInvariantBundle, machine-checked across all 2,955 scheduler theorems, including priority inheritance and liveness proofs with WCRT bounds.
Intrusive Dual-Queue IPC
seL4 keeps one queue per endpoint, its direction in the endpoint's state. seLe4n endpoints keep separate sendQ/receiveQ ends, linked through the TCBs, with O(1) mid-queue removal. A message is registers and a badge (IpcMessage): capabilities travel as addresses in the sender's frame and are resolved at the rendezvous (resolveExtraCaps), as seL4's lookupExtraCaps. WithCaps proves the transfer — 4,493 theorems including call-reply-recv composition proofs.
Capability Derivation Tree
As in seL4's mapping database, each CNode slot holds its derivation links — parent, first child, next and previous sibling — so the slot is the node and moving a capability moves its place in the tree. seLe4n proves the links agree with a ghost derivation tree (cdtLinksAgree). A delete splices its slot out and re-derives its children from its parent (spliceNode), so it never depends on whether the capability has derivations; cspaceRevokeCdtFinalising is seL4's cteRevoke loop, its check read before any write.
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. A non-interference proof for each of the 35 kernel steps, stated over the ObservableState projection of what a domain can observe.
Service Orchestration
Traditional microkernels have no kernel-level service concept. seLe4n adds a capability-indexed service registry with a dependency graph: serviceHasPathTo refuses any dependency that would close a cycle. Invariant proofs split into Acyclicity and Policy enforcement — 118 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 (41 decode-layer proofs) and
SyscallArgDecode (86 proofs, round-trip proofs included) 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 42-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 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 10 kernel object types compose through typed Capability references with bitmask-based AccessRightSet. Every object lives in one store in SystemState, a verified RHTable keyed by ObjId, and the CapDerivationTree enables composable revocation across the entire object graph — 1,059 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 1,526 theorems
across 24 modules. The DomainFlowPolicy
framework provides security guarantees that go beyond traditional binary high/low models:
- A non-interference proof for every kernel step — one for each of the 35 constructors of the
NonInterferenceStepinductive, and 39 more for cross-core operations under SMP - 52 operations classified by enforcement level, 67 once the per-core cross-core wrappers join them
- 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:
- Fixed slot arrays: a CNode's slots are written in place, as seL4's
cte_t - Revocation as seL4's
cteRevoke: the first child is deleted until none is left - Derivation links in each slot, proven to agree with the derivation tree
- 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 of the 419 production Lean modules. All 17,336 theorems in them are type-checked, and the in-tree testing framework builds alongside, outside these figures. 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.
NIGHTLY_ENABLE_EXPERIMENTAL=1 ./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 (includes the host Rust lane and docs sync) |
./scripts/test_full.sh | 0 + 1 + 2 + 3 | Full verification — invariant/theorem changes |
NIGHTLY_ENABLE_EXPERIMENTAL=1 ./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 42 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.
All 42 syscalls have corresponding safe Rust wrappers in sele4n-sys.
Project Structure
419 Lean modules, 73 test and CI scripts, and 256 documentation files with specifications, ADRs, and roadmaps.
Main, built by Tier 1 through SeLe4n.Platform.Staged)@[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 kernel and its staged modules. All 17,336 theorems across its 419 production Lean modules are checked; lake build alone builds the Main closure, so the staged hardware-binding and lock-primitive modules need the second target. The in-tree testing framework builds too, outside these figures. Zero sorry, zero axiom.
lake build
lake build SeLe4n.Platform.StagedRun 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 whole seLe4n syscall surface (all 42 syscalls). Builds on both ARM64 (real trap) and x86_64 (mock trap for host-based testing). After any change under rust/, run both Rust lanes: the host lane cannot see the HAL's aarch64-only code, which the cross-build lane builds for its real target.
# Host lane: build, tests, fmt, clippy
./scripts/test_rust.sh
# Cross lane: the HAL's real aarch64 target
./scripts/test_aarch64_cross_build.shContributing
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 — 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. On the hottest paths WS-ZA has since moved to seL4's own layout: queues linked through the TCBs and fixed CNode slot arrays.
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 (it has since grown to 42, and the wrappers cover all of them) including notification, compound IPC, scheduling contexts, and TCB management. Phantom-typed capabilities,
ARM64 register ABI layer, W^X enforcement, IPC buffer overflow handling.
unsafe confined to the svc #0 trap instruction.
Build → Freeze → Execute Pipeline Complete
Implemented the Build → Freeze → Execute pipeline with commutativity lemmas over the frozen store — the frozen operation set, 12 at completion, has grown since — 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/syscallEntry / syscallEntryChecked dispatch path with capability-gated routing. Rust ABI hardening with the SyscallId enum (since grown to 42 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 that now carries 84 @[extern] functions, and QEMU boot verification. BCM2712 memory map with 48-bit VA / 40-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. Phases SM0–SM9 have landed, closing with declassification completion; WS-RR (SMP release readiness) closed at v0.35.203, and SM10, the release closure, now waits on WS-BP, the bare-metal boot path: BP0–BP7 have landed and BP8 is under way — the Lean-linked image boots on all four PEs of QEMU’s virt board on every PR.
WS-ZA: A Syscall That Allocates Nothing In Progress
seL4 allocates nothing on a syscall. When the workstream was registered, the exerciser that counts heap allocations on QEMU’s virt read 118 for one notification signal. The signal round trip now reads 0, and the wait, IPC that blocks or rendezvouses, reply-receive, yield, the thread and scheduling-context invocations, and page map and unmap have followed: run, endpoint, notification and reply-waiter queues are linked through the TCBs, a CNode’s slots are a fixed array holding their own derivation links, and objects change in their slots.
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.