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 41 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.45. The kernel model is feature-complete with 41 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 and the bare-metal boot path (WS-BP) as the active workstreams.
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
10 composable kernel object types: TCB, Endpoint, Notification, CNode, VSpaceRoot, Untyped, SchedContext, Reply, Frame, PageTable. 650 theorems across Object (282) and State (368). 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
2,070 theorems across 52 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
315 theorems across 14 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 (31 theorems), Defs (57 theorems), and a Preservation suite (108 theorems across 7 files). Strict revocation via cspaceRevokeCdtStrict.
IPC & Dual-Queue
Deeply modularized across 69 files with 3,625 theorems. Intrusive dual-queue endpoints split into Core, Transport, and WithCaps. 655 structural invariant proofs, 40 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 193 theorems across 8 modules. RHTable provides O(1) amortized insert, lookup, and erase with open addressing and linear probing. 48 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,727 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 41-syscall seLe4n ABI, while the kernel-side sele4n-hal supplies the ARM64 hardware abstraction layer. sele4n-types defines a 41-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 hash map — O(1) hot paths, 193 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 — all 41 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, 650 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 193 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 — 193 theorems across 8 modules, with 48 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 2,070 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 —
3,625 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. A non-interference proof for each of the 35 kernel steps, 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 — 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 (24 decode-layer proofs) and
SyscallArgDecode (65 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 41-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. 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 — 650 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,727 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:
- 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 of the 346 production Lean modules. All 14,305 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 41 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 41 syscalls have corresponding safe Rust wrappers in sele4n-sys.
Project Structure
346 Lean modules, 71 test and CI scripts, and 252 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 14,305 theorems across its 346 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 41 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 — 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 (it has since grown to 41, 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 41 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 85 @[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.
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.