l4v: the seL4 specifications and proofs written in Isabelle/HOL

A proof repository, not a kernel source tree

l4v is the L4.verified git repository, and it contains formal specifications and proofs for the seL4 microkernel rather than the kernel code itself. Most of the proofs are conducted in the interactive proof assistant Isabelle/HOL, and the README points readers to the Isabelle website and documentation for an introduction. The separation matters for anyone considering adoption. The C implementation lives in the separate seL4 repository, and the design-level specification and the preprocessed C code that Isabelle reads are generated from other files rather than tracked directly here. So l4v is the verification side of a two-part arrangement: a real kernel implementation on one side, and a formal account of that implementation on the other, connected by a translation step that a human has to trust as much as the proofs themselves.

The spec/ tree holds several models of the same kernel

The specifications are not one document but a stack. spec/abstract/ is the functional abstract specification of seL4, and spec/sep-abstract/ is an abstract specification for a reduced version of seL4 configured as a separation kernel. spec/haskell/ is a Haskell model of the kernel kept in sync with the C code, and spec/machine/ is the machine interface that the two specifications share. spec/cspec/ is the entry point for automatically translating the C code into Isabelle. spec/capDL/ is a specification that abstracts from memory content and concrete execution behaviour and models the protection state in terms of capabilities, corresponding to the capability distribution language used to initialise user-level systems on top of seL4. spec/take-grant/ is a formalisation of the classical take-grant security model applied to seL4, and it is explicitly not connected to the kernel code.

The proof/ tree names the properties that get checked

The proofs are organised by the property they establish, and the directory names read like a table of contents for the verification effort. proof/invariant-abstract/ holds the invariants of the abstract specification. proof/refine/ is the refinement between the abstract and design specifications, and proof/crefine/ is the refinement between the design specification and the C semantics. proof/access-control/ contains the integrity and authority confinement proofs, and proof/infoflow/ the confidentiality and intransitive non-interference proofs. proof/asmrefine/ is the Isabelle/HOL part of the binary verification, with the tool side under tools/asmrefine/. proof/drefine/ is the refinement between capDL and the abstract specification, proof/sep-capDL/ a separation logic instance on capDL, and proof/capDL-api/ separation logic specifications of selected seL4 APIs. Two directories carry their own claims: camkes/ is an initial formalisation of the CAmkES component platform, marked work in progress, and sys-init/ is a specification of a capDL-based user-level system initialiser with a proof that the specification leads to correctly initialised systems.

lib/ and tools/ hold the reusable machinery

Not all the intellectual work is in the theorems. lib/ collects generic proof libraries, proof methods and tools, and the README lists what is in there: further libraries for fixed-size machine words, a formalisation of state monads with nondeterminism and exceptions, a generic verification condition generator for monads, a recursive invariant prover called crunch, an abstract separation logic formalisation, a prototype of the Eisbach proof method language, and a prototype levity refactoring tool. tools/ holds the larger self-contained tools. tools/c-parser/ is a parser from C into the Simpl language in Isabelle/HOL and includes a C memory model. tools/autocorres/ is an automated, proof-producing abstraction tool from C into higher-level Isabelle/HOL functions built on that parser. tools/haskell-translator/ is a Python script that converts the Haskell prototype into the executable design specification.

Running the proofs: one command and an architecture variable

With Isabelle installed and configured, the documentation says a full test of the proofs for seL4 on the ARM architecture can be run from the l4v directory with a single command:

    L4V_ARCH=ARM ./run_tests

The environment variable selects the target, and the README lists the accepted values as ARM, ARM_HYP and others. The machine requirements are given just as plainly. Almost all proofs should work within 4GB of RAM. Proofs involving the C refinement will usually need the 64-bit mode of polyml and about 16GB of RAM. The work distributes reasonably well over multiple cores, with up to about eight cores useful. That last figure is the practical planning point: a full run is a machine-hours decision, not a command you fire and forget before lunch.

Setup is a repository workflow, and clones are discouraged

The README is unusually direct about installation. This repository is meant to be used as part of a Google repo setup, and instead of cloning it directly you are asked to follow the directions for software dependencies and Isabelle installation in docs/setup.md in the docs directory. That instruction exists for a reason. The proof tree pulls in generated artifacts, in particular the C code preprocessed into a form that Isabelle can read, and that code comes from the seL4 repository rather than from l4v itself. A manual clone gives you a tree with holes in it. The repository also documents its own conventions and style under docs/, and CONTRIBUTING.md is the entry point for people who want to add to it, with a separate license file, CODE_OF_CONDUCT.md and CONTRIBUTORS.md at the root.

Releases are named after the kernel they cover

The version history answers the question a new user asks first, which is which kernel these proofs describe. The tags are seL4-16.0.0 for proofs of seL4 16.0.0, released on 2026-07-22, preceded by seL4-15.0.0 on 2026-03-31 and seL4-14.0.0 on 2025-11-25. The last push to the repository was on 2026-10-20, so the tree moves ahead of the newest tag. Continuous integration is visible in the README as several workflow badges, one for pushes, one for deploying the proofs, one for a weekly clean run and one for external repositories, plus a second pair for the MCS branch. The README also carries a Zenodo DOI badge, which is the archiving route for a formal artefact where the version that was checked is the version that matters.

Where l4v is the wrong tool

There are two honest alternatives, and they answer different questions. The first is the pragmatic one: run the kernel, test it, and use static analysis and fuzzing on the implementation. That gives evidence about the cases you exercised, quickly, without a proof effort, and for most product decisions it is the right trade. The difference in approach is that a theorem holds for every input and every execution, while a test holds for the inputs you thought of, and the price of the theorem is a proof session that needs the Isabelle environment, the repository workflow and real memory. The second alternative is the executable model already inside this tree. spec/haskell/ is a model of the kernel kept in sync with the C code, and the Haskell prototype plus the translator turns it into the executable design specification, which is far easier to run and experiment with than a proof. If your question is what the kernel does on a particular trace, the model answers it faster; if your question is whether it always does, you need the proof.

Editorial conclusion

l4v fits researchers, kernel engineers and standards bodies who need a machine-checked account of what seL4 does, who can budget the machine time the C refinement needs, and who are prepared to learn the Isabelle/HOL proof conventions before reading a theorem. It does not fit an application team that just wants to run seL4, and it does not fit a reviewer looking for a fast verdict from tests or static analysis, because a proof session is a different kind of artefact. Before starting, follow docs/setup.md rather than cloning the repository, decide which architecture you will set in L4V_ARCH, and note that the proof releases track the kernel, with seL4-16.0.0 tagged on 2026-07-22 and the last push to the repository on 2026-10-20.

Frequently asked questions

Official sources

1. Issues
2. Project website
3. README
4. Releases
5. seL4/l4v on GitHub