Reconnaissance · separation kernels & hypervisors

Proved Ground

We built a separation kernel, then asked the field whether any of it was new. The answer was no — on every axis we probed, and in several cases by work that solves the same problem more deeply. This page is what that search returned: who has already closed which guarantee, what state it is in, and the limitation that still matters. The negative result is the deliverable, not the consolation.

The map The case study Source Documentation

Why trust the map

It was assembled by someone who had to solve each problem first. Reading tells you what exists; building tells you what to ask.

The instrument

Baleen — a static-partitioning kernel for AArch64/EL2 in Rust, … machine-checked harnesses carried as a required gate. Four weeks old, and complete as research rather than continuing as a project. §02 is its own honest picture.

What it is not

A product pitch. For a device worn by a person, the answer below is seL4, and the fact that we wrote one of the candidates is not an argument.

Frozen A snapshot as of 2026-08-13, and it is not maintained. Every row was true on its date and several will not be by the time you read this — seL4's AArch64 confidentiality proof and its Arm MCS port are both in flight, and either landing changes a row below. ★ Treat the dates as the claim's expiry, not its authority, and check the linked source before relying on any row. The generated figures in §02 are a different matter: they are derived from this repository's own gates and cannot drift.

01 — The map

Every guarantee we needed was already closed by somebody.

Each row is a requirement a mixed-criticality system actually has, the project that owns it, and the caveat that decides whether you can rely on it. Read the last column — "verified" is never a single fact, and the architecture, the artifact and the proof's reach are usually where the answer lives.

★★ There are two status columns because there are two different questions, and collapsing them into one chip is how the first version of this table misled. Ground taken? is a question about papers, and a paper's result is permanent — SeKVM proved what it proved in 2021 and always will have. Buildable today? is a question about repositories, and repositories perish. Three rows below are proved-and-unbuildable, which is exactly the combination a single status chip cannot express.

⚠ This does not disturb the decision in §04. That rests on seL4 and libvmm, and both are live — checked against their repositories, not against a survey.

Hand-checked These are facts about other people's projects, so no gate here can police them and none pretends to. Each row carries the date it was last verified and a link to the source. They rot — seL4's Arm MCS proof landing would change a row below — so treat a stale date as a warning, not a detail. This is the opposite discipline from §02 and §03, which are generated and cannot drift.

Requirement	Who owns it	Ground taken?	Buildable today?	The limitation that matters
Microkernel functional correctness	seL4 seL4/seL4 · verified configurations	proved	live	Abstract spec → executable spec → C. Deployed and flown — DARPA HACMS, where the Red Team failed to compromise Boeing's Unmanned Little Bird in flight. ⚠⚠ Verification is not uniform across architectures, and AArch64 is the weakest mainstream target. ARM 32-bit has functional correctness, integrity, confidentiality and binary correctness. RISC-V 64 has functional correctness (no fast path), integrity and confidentiality. AArch64 has functional correctness and integrity — neither of the other two. ★ It is the architecture most people ship on.
Mixed-criticality temporal isolation	seL4 MCS docs · Proofcraft	partial	live	Scheduling contexts: capability-based access to CPU time with enforced execution bounds. Functional correctness proved on RISC-V; the Arm 64-bit port is in progress under DARPA PROVERS. ★ The one row whose answer today is "not yet, on your architecture."
Verified hypervisor on multicore Arm	SeKVM SOSP 2021 · repo SeKVM-4.18, last push 2021-09-18	proved	dormant	The SOSP 2021 result — verified on Arm relaxed memory hardware — is permanent. The artifact is not: pinned to Linux 4.18 and untouched since 2021, with its companion QEMU frozen at 3.0. ★ The clearest case for two columns: the ground is taken, the code is a museum piece.
Verified preemptive scheduler with temporal isolation	Virtual Timeline PACMPL 4(POPL), POPL 2020 · 10.1145/3371088	proved	paper only	Liu, Rieg, Shao, Gu, Costanzo, Kim & Yoon — the CertiKOS group. The formal abstraction for exactly this, and it occupies the problem this project had identified as its sharpest open one, six years earlier and in a stronger form.
Linux guest beside a small analyzable partition	libvmm / CAmkES VM repo pushed 2026-08-13 · au-ts/libvmm	shipping	live	A VMM for seL4 under Microkit, booting Linux guests on Arm. ⚠ Confirm GICv3 emulation for your board — a live discussion item rather than a settled feature, and support is per-platform.
The framework you would build the system with	seL4 Microkit repo pushed 2026-08-14 · seL4/microkit	shipping	live	★★ Written in Rust — 465 KB Rust to 187 KB C, pushed the day this row was written, with recent commits that are Rust idiom cleanups. rust-sel4 is live too. ★ The verified kernel is C; the layer you compose a static system with is not. Choosing seL4 does not mean leaving Rust.
Multi-tenant compute isolation	Firecracker repo pushed 2026-08-13 · firecracker-microvm	shipping	live	Apache-2.0, Arm and x86, at AWS scale. Not formally verified as a whole, but industrially proven — which for this requirement is the stronger claim.
Keeping a formal model honest against the code	Cedar repo pushed 2026-08-13 · arXiv 2407.01688	solved	live	An executable Lean model — 3.8 MB Lean to 1.2 MB Rust — with differential random testing as a release gate: millions of inputs through both, outputs compared. 4 bugs from the proofs, 21 more from DRT and property-based testing. ★ A template, not a research problem.
Verification affordable as a CI gate	Kani, in production arXiv 2607.01504 · repo pushed 2026-08-14	shipping	live	Running in production CI on Firecracker — the VMM behind Lambda and Fargate — plus s2n-quic, Hifitime, and the Rust standard library. ★ Existence proof that proving is a budget line, not a campaign.
Whether diverse assurance arguments are independent	Knight & Leveson; Littlewood & Wright; Rushby Knight & Leveson 1986	settled	paper only	They are not. 27 independently written versions over 1M test cases showed correlated failure far above chance; Littlewood & Wright model dependence between a testing leg and a formal verification leg specifically. Replicated across NASA and nuclear programmes. ⛔ A verification portfolio is not the union of its tiers.
Static-partitioning hypervisor on Arm	Bao repo pushed 2026-08-10 · bao-project	shipping	live	Real hardware, real deployments, actively maintained. The architectural niche this project occupies was already well populated before it started, and still is.
Static-partitioning hypervisor, the older reference	Jailhouse last commit 2023-01-16 · last push 2024-05-18 · siemens/jailhouse	shipping	dormant	⚠ Not archived, 1,950 stars, and not moving. A legitimate architectural reference — not a live option to build on. ★ Note the direction: dormant, but it ran on real silicon in production. That still beats active-but-never-left-the-emulator.
A verified hypervisor written in Rust	RayNu-V, RVM RayNu-V page read 2026-08-13 (v0.1.1) · RVM not read	unverified	not assessed	RayNu-V pairs Verus and Kani on an x86/VMX/EPT hypervisor and states an EPT isolation theorem — but its page lists milestones M0–M6 with none completed, so the theorem is the plan's endpoint. It began 2026-07-18, three days after this project, and explicitly rejects forbid(unsafe_code). ★ Convergent, not derivative — and a reason "first verified hypervisor in language X" is worthless as a claim. ⚠ RVM has not been read; its verification is described as planned.
A verified hypervisor under compute-heavy simulation	— nobody, and correctly so reasoning, not a citation	no case	—	A hypervisor does not make cores faster. Isolation is not that workload's bottleneck, the binding constraint is memory bandwidth, and Firecracker already owns multi-tenant isolation. ★ Kept as a row because the idea is attractive, recurs, and is wrong.

How this went wrong Within a day of first publication this table had eight defects, and every one came from citing something nobody had opened. Liveness taken from a 2023 survey (Jailhouse had been still for a year by then). A machine-checked theorem taken from a search snippet that was describing a document's plan. A binary-verification claim that held for ARM 32-bit and not for AArch64. A paper dated to the wrong year. ★★ Two rules came out of it. A row citing a PAPER is safe, because a paper's content never changes; a row about whether a PROJECT IS ALIVE is not, and its primary source is the repository. And a date implies verification — where there was none, the date was rigour-shaped decoration.

Ground taken? provedmachine-checked settledestablished and replicated shippingindustrially proven, not fully verified partialproved, but not on every architecture unverifiedclaimed; not established no casedeliberately unoccupied

Buildable today? liverepository active — date on the row dormantreal, not moving — check before building on it paper onlyno artifact assessed; irrelevant to the novelty question — state is written in the chip, never carried by colour alone

02 — The instrument

Half the shipped code is machine-checked. The other half is a thin layer that cannot be.

A map is only worth what the person assembling it knows, so here is that person's own work, held to the same standard. Verification tools reach code inside the workspace. hv-metal is deliberately excluded — it needs unsafe for MMIO and assembly, so no prover links it and it is held to boot witnesses instead.

Generated Every figure in this section and the next is read from assurance-data.json, which cargo xtask site-data derives from the same gates that police the repository — and cargo xtask ci fails if the committed copy is stale. These cannot drift from the artifact they describe, which is the only reason this page is allowed to state them as numbers.

Under the proof fence
seven crates forbid(unsafe_code) — enforced by the compiler, not by convention

Outside it
the fenced unsafe layer, witnessed by boot markers only

Evidence by subsystem

Five methods with different reach. A row is only as strong as what the chips actually say — and two of the columns share an input generator, which is how a real defect survived four of them.

Subsystem	Enumerator	Kani	Verus	Fuzz	Boot

Harnesses cluster where the isolation argument is load-bearing.

Kani harnesses by module. The shape is the honest one: the emitter and the model's invariants carry the weight, because that is where a wrong answer becomes a cross-domain leak.

03 — What this settles

A reconnaissance that ends without a decision has not finished.

The map is not neutral. It was assembled to answer specific questions for a specific project — a differentiable simulation SDK whose capstone is a person-specific powered exoskeleton — and these are the answers.

The device

seL4, with Microkit and libvmm — on a board seL4 supports.

A powered exoskeleton is a mixed-criticality system: a learned policy that cannot be trusted by construction, beside a safety monitor whose envelope must hold anyway. For something worn by a person, a proved-and-flown kernel beats a four-week-old single-core one that has never left QEMU. That we wrote the second is not an argument.

⚠ Go in knowing what AArch64 actually buys you. It has seL4's functional correctness and integrity proofs — not confidentiality, and not binary verification; both exist on ARM 32-bit, and confidentiality also on RISC-V. It is still far more than this project has, and it is less than the headline "seL4 is verified" implies on the architecture you would ship.

The datacentre

No verified hypervisor under simulation workloads. Refuted, twice, and recorded so it is not re-proposed.

Isolation is not the bottleneck, memory bandwidth is; a hypervisor cannot improve it and slightly worsens it. The single-tenant variant is weaker still — there is nobody to isolate from.

The one thing still open

Proved temporal isolation on Arm. seL4 MCS has it on RISC-V; the Arm port is in progress.

The only requirement on this page whose answer is "not yet, on your architecture". Everything else is a matter of integration rather than research — which is the most useful thing the search established.

04 — Where this project stopped

A map assembled by an artifact should show that artifact's edges.

Baleen is complete as research and paused as a project. These are not a roadmap — the decision above routes around them. They are the honest statement of where it stopped, and they are why it is not a thing to build on.

Needs hardware

No silicon. Every metal result is QEMU. A board probe exists and has never run on a board.
SMMU translation caching — witnessed on Arm's simulator, not on the boot path.
VMID tagging and stage-2 TLBI are not boot-witnessed; QEMU caches nothing, so it structurally cannot show them.
The EL2 loader/cache contract — a bring-up assumption, not a checked property.

Needs a different technique

Scheduler latency bound. A claim about unbounded runs, so no larger bounded harness reaches it. The formula itself is settled — an earlier one was false at quantum = 1 and has been replaced by a bound derived from the scheduler's ranking function, asserted across a 75-row grid. What is missing is the tier: that is simulation evidence, and the bound is sound-but-loose on 46 of the 75 rows. ⚠ Virtual Timeline (POPL 2020) already owns this problem — see §01.
Proportional fairness. A statement about a limit, so not bounded-depth either.
The model-to-metal step is a construction argument narrowed by compile-time assertions, because no prover links the metal.

Needs a consumer first

Grant revocation. Stage-2 is emitted once, so ending a grant does not disturb an emitted descriptor — fine today, a surprise for anything expecting revocation to bite.
Monitor freshness. A starved observer cannot tell silence from health; the fix needs a telemetry format that may not be this project's to define.
Actuator and sensor I/O. Groundwork only — no real device is driven, which is the functional gap between a demonstration and a device.

Two disciplines, kept apart deliberately. §02 and §03 are generated by cargo xtask site-data from the gates that police the repository, and cargo xtask ci fails if they are stale — so they cannot drift. §01 and §04 are hand-checked facts about other people's work, dated per row, and they will rot. Conflating the two is the one way this page starts lying, which is why it says so twice.

Assembled from the development of Baleen. Apache-2.0 / MIT. Corrections are welcome and are the point — open an issue if a row is out of date.