For its verified configurations, seL4's proof establishes that the C code implements the abstract specification exactly and nothing more: no buffer overflows, null dereferences, memory leaks, undefined behaviour. The proof cannot establish the specification is right, rests on seven published assumptions, and covers five named single-core configurations carrying different properties, not seL4 in general. A proof is a scope statement.
Ross Jones — Founder, The Hopium Lab. Last modified 22 July 2026. Written from the proofs, not from deployment; engineering commentary, not legal advice.
What exactly did the seL4 proof establish?
Functional correctness, in the formal sense: for verified configurations, the C code behaves precisely as the seL4 specification describes and does no more. The seL4 proofs page enumerates five families — functional correctness, integrity, confidentiality (information flow), availability, binary correctness — chained by refinement: abstract specification → executable specification → C implementation → binary, each link a separate obligation with its own scope. On its own, "seL4 is verified" carries no information.
Functional correctness eliminates whole defect classes rather than thinning them. The implications page lists them: buffer overflows, null pointer dereferences, pointer errors, memory leaks, arithmetic overflows, undefined behaviour. Gone, mathematically, inside the verified configuration.
The original result (Klein et al., SOSP'09, October 2009) covered 8,700 lines of C and 600 of assembler with roughly 200,000 lines of Isabelle/HOL and about 20 person-years; Trustworthy Systems now puts the corpus at nearly a million lines of proof steps. For the full stack cite the 2014 ACM TOCS consolidation, since SOSP'09 predates the security and binary proofs.
Get the priority claim right. seL4's own FAQ claims the first and still only "general-purpose OS kernel with a full code-level functional correctness proof" — every qualifier load-bearing, since Bevier's Kit (IEEE TSE 15(11), November 1989) was machine-checked at machine-code level twenty years earlier.
What does the proof assume rather than prove?
Seven assumptions, named and published by the seL4 team on one page: around 340 lines of hand-written assembly per architecture; hardware working to specification and untampered; in-kernel cache, cache-colouring and TLB management; boot code, roughly 1,200 lines outside the theorem; the kernel's virtual-memory behaviour during execution; DMA, where the CPU and MMU are assumed the only devices touching memory directly; and hardware information channels, applying to the confidentiality proof alone. Isabelle/HOL itself stays in the trusted base, mitigated by LCF architecture rather than eliminated.
The compiler used to sit on that list. On architectures covered by binary verification it no longer does — seL4's own wording is that the compiler and linker need not be trusted there. Translation validation (Sewell, Myreen & Klein, PLDI 2013) proves refinement between C and binary semantics with SMT solvers, one code sequence at a time, per build — not a verified compiler, not CompCert. Stated limits: unmodified gcc 4.5.1 at optimisation level 1, most of the kernel at level 2, assembly and volatile hardware accesses omitted. RISC-V 64 was announced as the first 64-bit architecture verified to binary code in May 2021, but the current verified-configurations matrix lists binary correctness only for AArch32. Trust the matrix over the announcement.
An assumption list is not a defect list. An assumption list is what shrinks the thing you must trust from thousands of lines of C to a few named pieces a human can audit.
Does "seL4 is verified" mean the same thing on every architecture?
No, and the verified configurations matrix is the most under-cited page in the project.
| Configuration | Functional correctness (C) | Integrity + availability | Confidentiality | Binary correctness |
|---|---|---|---|---|
| ARM AArch32 (EL1, no FPU, no hyp) | Yes, incl. fast path | Yes | Yes | Yes, for C functions with C-level verification |
| RISCV64 (HiFive Unleashed, no fast path) | Yes | Yes | Yes | Achieved 2021, not listed in the current matrix |
| AArch64 (ARMv8-A, EL2, FP enabled) | Yes, incl. fast path | Yes | In progress | No |
| ARM_HYP (AArch32 with virtualisation, EL2) | Yes | No | No | No |
| X64 (PC99, no fast path) | Yes | No | No | No |
One row — AArch32 — carries the complete story, and it is the oldest, most constrained configuration on the list. The x86-64 row — the architecture most people picture on hearing "verified microkernel" — stops at the C level.
Every verified configuration is also uniprocessor: the matrix does not say so, because SMP seL4 is not on it. seL4 avoids in-kernel preemption except at a few defined points precisely so the proofs never reason about concurrency. Multicore seL4 ships unverified, the gap that bites hardest in practice.
Why doesn't the confidentiality proof mean seL4 has no leaks?
Because the confidentiality proof is stated against a modified kernel, and its security property permits specific leaks by construction. The property is also scoped to security domains of seL4's domain scheduler, not to arbitrary threads — two threads inside one domain get nothing from it. Murray et al., IEEE S&P 2013 proved noninterference for a seL4 variant whose scheduler was modified to do fixed static partition scheduling; the original leaked through its scheduling decisions, never having been designed to enforce isolation. Further conditions: only the timer interrupt enabled, a wellformed access-control policy consistent with the initial state, inert copies of subject-crossing capabilities, and a largely deterministic abstract specification.
The property statement concedes ground deliberately: the global static schedule may be known by every partition, so the theorem does not prevent one partition knowing another exists, nor a newly scheduled partition inferring that its predecessor burned its timeslice.
Timing is the sharper limit: the information-flow work covers in-kernel storage channels, not microarchitectural timing channels. Proving the Absence of Microarchitectural Timing Channels (Buckley, Sison et al.) attacks that gap, building on the storage-channel proofs.
The frontier moved this year. Proofcraft verified a semi-static domain-scheduler API, shipped in seL4 15.0.0 on 1 June 2026, relaxing the static schedule the 2013 proof depended on; and on 29 June 2026, a first functional-correctness verification of seL4 with MCS, on RISC-V.
The guarantee is exactly as strong as the property statement, and property statements are written by people making trade-offs under deadlines. Read the property, not the headline.
Can a proof tell you the specification is right?
No. No proof can, and the seL4 team says so more plainly than its admirers do. Asked whether seL4 has zero bugs, the implications page answers: "Yes, of course, and no, of course not." Specifications contain surprises, and security must be formally defined before it can be proved.
Twenty person-years buys certainty that the code matches the specification. Nothing in the method buys certainty that the specification matches the world.
What transfers to AI systems, where nothing has a specification?
The interrogation protocol transfers. The proof technique does not. An LLM has no formal specification and no deterministic implementation — no artefact to prove anything against. Pretending otherwise makes the analogy embarrassing.
A verification scope is four things: the property, the specification it is stated against, the assumptions it rests on, and the configuration it holds in. Ask those four questions of an eval suite and most fail on the second. The property is an adjective. The specification does not exist. The assumptions are unwritten. The configuration is a product name rather than a build.
Coverage is the distinction that matters. Testing checks behaviour on a finite set of cases; formal verification reasons over the entire input space of a model (arXiv:2104.14235). Total coverage is bought by shrinking the modelled system until reasoning stays tractable — which is why verification lives at small scale.
Two honest moves remain. Put the guarantee in a small checkable component outside the model — isolation of untrusted components is seL4's actual value proposition and the structural analogue of sandboxing a probabilistic system, a boundary question of its own. And where a sample is all there is, use one carrying a calibrated coverage statement: conformal prediction sits between an eval and a guarantee, Guaranteed Safe AI as the anchor.
An eval set is a sample of behaviour. A guarantee is a property of structure. Reporting a pass rate as if it were coverage is a category error, not a rounding error.
What goes wrong when nobody writes the scope down?
The claim outlives its scope and nobody notices. Six recurring shapes, named — unnamed failure modes never get engineering time.
- Configuration laundering. A property proved for one configuration gets quoted for the product: binary correctness on AArch32 while shipping x86-64; an eval passed on one pinned model id after a silent provider update.
- Assumption erasure. The caveat list stays in the paper while the claim travels alone. Every seL4 misquote works this way.
- Trusted-base creep. A component lands inside the boundary the proof never covered — a DMA-capable peripheral, or a new tool an agent can call.
- Specification drift. The property statement gets weakened until the system passes, and nobody re-reads it.
- Sample-as-guarantee. A pass rate on a held-out set reported as coverage.
- Frame contamination. The held-out set leaks into training, so the sample stops being a sample.
My own auditor, Diablo, runs 17 published categories plus an adversarial synthesis pass. First-party tooling: my code, my method, no accreditation, no independence claim — independence is an accredited property under conformity-assessment standards, not a marketing word. The taxonomy sits in the open, in production-readiness categories and behind Go / No-Go, for the reason seL4 publishes assumptions: a method nobody can argue with is a method nobody should trust.
What should you write down before claiming anything is verified?
A scope statement, before the claim leaves the building.
VERIFICATION SCOPE STATEMENT — v1.0
The Hopium Lab · 22 July 2026 · take it, fork it, argue with it
Supports a conformity case. Does not confer one. Not legal advice.
PROPERTY One falsifiable sentence. What is claimed to hold.
SPECIFICATION The versioned artefact the property is stated against.
If none exists, write NONE — the absence is the finding.
ASSUMPTIONS Everything trusted rather than established. Numbered.
CONFIGURATION Exact build, architecture, model id, params, core count.
EVIDENCE PROOF | EXHAUSTIVE_TEST | CALIBRATED_SAMPLE | SAMPLE | NONE
COVERAGE SAMPLE: n, the frame, what the frame excludes.
CALIBRATED_SAMPLE: coverage level and method.
PROOF: the model it ranges over, and that model's size.
EXPIRY The event voiding the claim — retirement, config change,
dependency bump, new DMA-capable device.
OUTSIDE Everything the claim says nothing about. Longest section.
(The scope is the first four fields. The rest is how you report it.)
REJECT THE STATEMENT IF:
[ ] PROPERTY is an adjective — "safe", "robust", "aligned", "verified"
[ ] SPECIFICATION names a document nobody has opened this quarter
[ ] ASSUMPTIONS is empty. Empty means unexamined, never zero
[ ] CONFIGURATION names a product rather than a build
[ ] EVIDENCE says PROOF while COVERAGE reports a pass rate
[ ] OUTSIDE is shorter than PROPERTY
The OUTSIDE check catches most people. Exclusions shorter than claims is the signature of a statement written for a buyer; seL4's willingness to publish a long one is the practice worth copying, well ahead of the theorem-proving.
Stop asking whether a system is verified. Ask which property, against which specification, under which assumptions, in which configuration — and watch most claims die on the second. Same instinct as the replay test. Can you rebuild the answer without calling the model? If not, you don't have a system. You have a demo with a try/except around it.