seLe4n — A Microkernel Written in Lean 4

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. During the Freeze phase, the one-way freeze function converts the builder state into a FrozenSystemState where all RHTable fields become FrozenMap structures and CNode slots become CNodeRadix flat radix arrays with zero-hash O(1) lookup. During the Execute phase, the frozen state serves all 25 syscalls with value-only mutations — 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. 18 commutativity theorems prove that 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.28.0. The kernel model is feature-complete with 25 syscalls spanning IPC, scheduling, capabilities, memory management, notifications, information-flow control, and service orchestration. A companion Rust workspace provides safe, no_std wrappers for all 25 syscalls. Hardware platform bindings for the Raspberry Pi 5 are structurally in place, pending refinement phase closure.

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.

Rust User-Space Wrappers 3 crates · 25 syscalls · zero unsafe in sele4n-sys

sele4n-types Core types · no_std · zero unsafe sele4n-abi ARM64 ABI · svc #0 trap sele4n-sys Safe wrappers · 25 syscalls

API Surface

Kernel API SeLe4n/Kernel/API.lean

Core Subsystems

Scheduler 20 files · priority inheritance · liveness Capability 5 files · 118 thms IPC 20 files · donation · timeout Lifecycle 4 files · suspend/resume Service 7 files · registry · interface FrozenOps 5 files · 18 commutativity thms RadixTree 4 files · CNodeRadix SchedContext 10 files · CBS scheduling

Information Flow 9 files · 182 theorems

Policy Projection Enforcement Soundness · Wrappers Invariant Composition · Helpers · Ops

Hardware Abstraction 10 files · IPC buffer validation

VSpace VSpaceBackend Adapter TLB Register Decode Syscall Decode

Foundations

Object Model Types · Structures State Builder FrozenState Prelude Machine Robin Hood 7 files · 179 thms

Platform Bindings

Contract Simulator RPi5

Prelude & Machine

16 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

7 composable kernel object types: TCB, Endpoint, Notification, CNode, VSpaceRoot, Untyped, SchedContext. 129 theorems across Object (76) and State (53). Objects compose through typed Capability references with bitmask AccessRightSet. The SystemState record aggregates all stores into a single immutable snapshot — HashMap-backed for O(1) access everywhere.

Scheduler

20 files spanning core operations, priority inheritance, and liveness proofs. RunQueue backed by HashMap Priority (List ThreadId) with HashSet 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

118 theorems across 5 modules. CNode slots backed by HashMap Slot Capability for O(1) operations. Node-stable Capability Derivation Tree with childMap : HashMap CdtNodeId (List CdtNodeId). Invariant proofs split into Authority (26 theorems), Defs (46 theorems), and Preservation (46 theorems). Strict revocation via cspaceRevokeCdtStrict.

IPC & Dual-Queue

Deeply modularized across 20 files. Intrusive dual-queue endpoints split into Core, Transport, and WithCaps. 76 structural invariant proofs, 27 endpoint preservation theorems, and 16 capability transfer proofs. Operations decomposed into CapTransfer, Endpoint, SchedulerLemmas, Donation, and Timeout.

Robin Hood Hash Map

Verified Robin Hood hash table implementation with 179 theorems across 7 modules. RHTable provides O(1) amortized insert, lookup, and erase with open addressing and linear probing. 30 bridge theorems connect the implementation to HashMap-compatible semantics. 56 preservation proofs and 40 lookup correctness theorems. Imported by Model.Object.Types — the verified foundation for all kernel hash-based data structures.

Information Flow

182 theorems across 9 deeply modularized files. Enforcement split into Soundness and Wrappers. Invariant proofs decomposed into Composition, Helpers, and Operations. 15 non-interference theorems with proven reflexivity and transitivity.

Service Orchestration

7 files. Graph-based lifecycle 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. Dependency-aware startup, shutdown, and restart.

Platform Layer

PlatformBinding typeclass defines runtime, boot, and interrupt boundary contracts. ExtendedBootBoundaryContract adds platform boot fields. 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

Three no_std Rust crates provide ergonomic, fully safe wrappers around all 25 seLe4n syscalls. sele4n-types defines 15 #[repr(transparent)] newtype identifiers, a 44-variant KernelError enum, 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, 179 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 HashMap 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 — 25 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, 129 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 179 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. All 16 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 — 179 theorems across 7 modules, with 30 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 HashMap-backed priority buckets, reducing candidate selection from O(t) total threads to O(k) priority levels. The schedulerWellFormed structural invariant is machine-checked across 20 files 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 — 223 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 HashMap-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. 15 non-interference theorems, 7-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 across 90 theorems.

Verified Hardware Boundary

Where traditional kernels leave register parsing unverified, seLe4n verifies the hardware-software boundary end-to-end. RegisterDecode (18 roundtrip proofs) and SyscallArgDecode (28 determinism proofs) 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 three no_std Rust crates with fully safe, typed APIs for all 25 syscalls. sele4n-sys introduces phantom-typed Cap<Obj, Rts> capabilities with compile-time rights tracking and W^X enforcement. The entire crate stack has zero unsafe except the single svc #0 trap instruction in sele4n-abi.

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 7 kernel object types compose through typed Capability references with bitmask-based AccessRightSet. All stores in SystemState are HashMap-backed for O(1) access, and the CapDerivationTree enables composable revocation across the entire object graph — 129 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 182 theorems across 9 modules. The DomainFlowPolicy framework provides security guarantees that go beyond traditional binary high/low models:

15 non-interference theorems — 12 standalone + 3 enforcement bridges
25 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 HashMap-backed CNodes
Strict revocation with explicit error reporting and context
Node-stable CDT with childMap HashMap 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
Lean toolchain integrity

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 .gitignore secret/artifact denylist
SHA-256 verified elan installer downloads
Tier-3 anchor checks against CI workflow semantics
Non-blocking CodeQL security baseline

Verification & Testing

seLe4n employs a multi-tiered verification strategy combining Lean's type-checker with runtime testing, ensuring correctness from proof to execution.

Tier 0

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.

./scripts/test_tier0_hygiene.sh

Tier 1

Build

Full Lean compilation across 270 parallel build jobs. All 2782 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.sh

Tier 2

Runtime

Trace sequence probes validate executable behavior against formal semantics. The negative-state suite tests malformed input rejection across IPC, capabilities, endpoints, and CSpace mutations. Information-flow runtime checks verify enforcement wrappers.

./scripts/test_tier2_negative.sh && ./scripts/test_tier2_trace.sh

Tier 3

Invariant 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.sh

Tier 4

Nightly

Determinism checks, experimental feature validation, and long-running invariant probes. Fixture-backed oracle testing. Catches subtle regressions that slip through faster tiers.

./scripts/test_nightly.sh

Test 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 25 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 25 syscalls have corresponding safe Rust wrappers in sele4n-sys.

Entry Point	Subsystem	Status
`Send` (ID 0), `Receive` (ID 1)	IPC	Stable
`Call` (ID 2), `Reply` (ID 3)	IPC	Stable
`CSpaceMint` (ID 4), `CSpaceCopy` (ID 5)	CSpace	Stable
`CSpaceMove` (ID 6), `CSpaceDelete` (ID 7)	CSpace	Stable
`LifecycleRetype` (ID 8)	Lifecycle	Stable
`VSpaceMap` (ID 9), `VSpaceUnmap` (ID 10)	VSpace	Stable
`ServiceRegister` (ID 11), `ServiceRevoke` (ID 12), `ServiceQuery` (ID 13)	Service	Stable
`NotificationSignal` (ID 14), `NotificationWait` (ID 15)	Notification	Stable
`ReplyRecv` (ID 16)	IPC (compound)	Stable
`SchedContextConfigure` (ID 17), `SchedContextBind` (ID 18), `SchedContextUnbind` (ID 19)	SchedContext	Stable
`TcbSuspend` (ID 20), `TcbResume` (ID 21)	TCB	Stable
`TcbSetPriority` (ID 22), `TcbSetMCPriority` (ID 23), `TcbSetIPCBuffer` (ID 24)	TCB	Stable
`cspaceLookupSlot`, `cspaceLookupPath`	Capability	Stable
`schedule`, `handleYield`, `timerTick`	Scheduler	Stable
`syscallEntryChecked`	Info-flow dispatch	Stable
`frozenLookupObject`, `frozenStoreObject`	FrozenOps	Stable

Project Structure

135 Lean modules, 25 test and CI scripts, and 204 documentation files with specifications, ADRs, and roadmaps.

seLe4n/

SeLe4n/

Prelude.lean — 16 typed identifiers, KernelM monad, HashMap bridges

Machine.lean — Register file, memory regions, MachineConfig

Kernel/

API.lean — Unified syscallEntry/syscallEntryChecked dispatch, apiInvariantBundle, 25 syscalls

Architecture/ — VSpace, VSpaceBackend, Adapter, TlbModel, RegisterDecode, SyscallArgDecode, IpcBufferValidation, Assumptions, Invariant, VSpaceInvariant (10 files)

Capability/ — Operations, Invariant/{Authority, Defs, Preservation} (5 files)

FrozenOps/ — Core, Operations, Invariant, Commutativity (5 files) — execution-phase typed lookups, value-only mutations, 18 commutativity theorems

IPC/ — DualQueue/{Core, Transport, WithCaps}, Operations/{CapTransfer, Donation, Endpoint, SchedulerLemmas, Timeout}, Invariant/{Structural, EndpointPreservation, NotificationPreservation, CallReplyRecv, Defs, QueueMembership, QueueNextBlocking, QueueNoDup, WaitingThreadHelpers} (20 files)

InformationFlow/ — Policy, Projection, Enforcement/{Soundness, Wrappers}, Invariant/{Composition, Helpers, Operations} (9 files)

Lifecycle/ — Operations, Suspend, Invariant/{SuspendPreservation} (4 files) — retype, suspend/resume, TCB management

RadixTree/ — Core, Bridge, Invariant (4 files) — CNodeRadix flat radix array for zero-hash slot lookup in frozen state

RobinHood/ — Core, Bridge, Set, Invariant/{Defs, Lookup, Preservation} (7 files, 179 theorems)

SchedContext/ — Types, Budget, Operations, PriorityManagement, ReplenishQueue, Invariant/{Defs, Preservation, PriorityPreservation} (10 files) — CBS scheduling contexts

Scheduler/ — RunQueue, Operations/{Core, Preservation, Selection}, Invariant, PriorityInheritance/{BlockingGraph, BoundedInversion, Compute, Preservation, Propagate}, Liveness/{BandExhaustion, DomainRotation, Replenishment, TimerTick, TraceModel, WCRT, Yield} (20 files)

Service/ — Operations, Interface, Registry, Registry/Invariant, Invariant/{Acyclicity, Policy} (7 files)

Model/ — Object/{Types, Structures}, State, Builder, FrozenState, FreezeProofs, IntermediateState (7 files) — three-phase state model

Platform/ — Contract.lean, Sim/, RPi5/

Testing/ — MainTraceHarness, InvariantChecks, StateBuilder, Fixtures

docs/ — Living specifications, ADRs, threat model, IF roadmap, and claim index evidence.

scripts/ — 25 test, CI, and documentation scripts

tests/ — InformationFlowSuite, NegativeStateSuite, TraceSequenceProbe, RobinHoodSuite, RadixTreeSuite, FrozenStateSuite, FreezeProofSuite, FrozenOpsSuite, TwoPhaseArchSuite, OperationChainSuite

rust/ — Rust workspace (3 crates, 25 syscall wrappers)

sele4n-types/ — 25-variant SyscallId, 15 newtypes, 44-variant KernelError, AccessRights · no_std · zero unsafe

sele4n-abi/ — ARM64 register ABI, MessageInfo, trap (sole unsafe: svc #0)

sele4n-sys/ — Safe syscall wrappers: IPC, CSpace, lifecycle, VSpace, notification, service, TCB · zero unsafe

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 seLe4n

Set 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.sh

Build & Verify

Build the entire kernel. All 2782 theorems are checked during compilation across 270 parallel build jobs. Zero sorry, zero axiom.

lake build

Run 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.sh

Build Rust Syscall Wrappers

The rust/ workspace provides safe, no_std wrappers around all 25 seLe4n syscalls. Builds on both ARM64 (real trap) and x86_64 (mock trap for host-based testing).

cd rust
cargo build
cargo test

Contributing

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.sh at minimum; test_full.sh for 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 — 7-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 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 18 commutativity theorems proving 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 25-variant SyscallId enum.

Refinement In Progress

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 Upcoming

Structural foundation is in place: PlatformBinding typeclass, MachineConfig, VSpaceBackend, RPi5 stubs with BCM2712 memory map and GIC-400 constants. 48-bit VA / 44-bit PA address space. Blocked on refinement phase closure.

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.