seL4, Meet Lean

A masterpiece, viewed from the outside

seL4 is a microkernel, about 10,000 lines of C, and it has a property almost nothing else in software has: a machine-checked proof that the C code does exactly what its specification says. The proof is not a sketch or a model of the code. It goes from an abstract specification, through an executable model written in Haskell, all the way down to the C semantics, and a computer checks every step.

The proofs live in a project called l4v, written in Isabelle/HOL. When I first opened it, the scale stopped me. The RISCV64 functional-correctness chain alone is about 220,000 lines of proof script and 14,000 lemmas. Behind that sit a C parser, a library of monads and Hoare logic, and years of careful human work.

Meanwhile, the Lean community has been doing something different and exciting. Mathlib grew into a giant shared library, Lean 4 is a real programming language as well as a prover, and a lot of young developers are learning to write proofs in it. So I asked a naive question:

If all of that verified seL4 infrastructure already exists, can we use it as a scaffold to bootstrap a Lean version? And if we can, could it widen the pool of people who can work on a great RTOS?

I did not want an opinion. I wanted a measurement: is it possible, and what does it cost in tokens and clock time? So I set up a cloud box, a repo, and a staged plan, and handed most of the keyboard to Claude Opus 5.5. Everything described here is in that repo: github.com/elevenarms/sel4-lean.

The map before the territory

l4v proves seL4 correct as a stack of refinements. Each layer is shown to behave like the one above it. Porting means rebuilding every box and every arrow in another prover.

flowchart TB
  A["Abstract spec
hand-written Isabelle"] -- "Refine: ~5,500 lemmas
plus invariants (AInvs)" --- E["Executable spec
Haskell model, translated"]
  E -- "CRefine: ~2,500 lemmas" --- C["C implementation
parsed into Isabelle"]

We broke the work into crawl, walk and run. Crawl was one thin vertical slice: one kernel function taken through every layer. Walk was the whole executable spec. Run is the proofs at full scale, which is where the real cost lives.

Crawl: run the original first

C0Before writing a single line of Lean, we made the Isabelle proofs pass on our own hardware: a 32-core cloud machine with local NVMe, inside l4v's own Docker image. The first attempt was killed for running out of memory. The second hit CPU-time budgets, because the timeouts count CPU seconds and we were using 32 threads. The third passed:

That turned out to matter more than I expected. Every later claim about "matching l4v" rests on having l4v's own built artifacts sitting on the same machine.

C2–C4A first proof in Lean

Next we rebuilt the foundations in Lean: l4v's nondeterministic state monad, Hoare triples, the corres refinement relation, and Lean versions of l4v's workhorse tactics wp, wpsimp and crunch. A small translator, hs2lean, turned the Haskell model of seL4's notification objects into Lean. Here is the translated cancelSignal:

def cancelSignal (threadPtr : PPtr TCB) (ntfnPtr : PPtr Notification) : Kernel Unit :=
  let isWaiting := fun ntfn =>
    match ntfn with
    | NTFN.WaitingNtfn .. => true
    | _ => false
  do
    let ntfn ← getNotification ntfnPtr
    assertH (isWaiting (Notification.ntfnObj ntfn)) "cancelSignal: notification object must be waiting"
    let queue' := deleteH threadPtr (NTFN.ntfnQueue (Notification.ntfnObj ntfn))
    let ntfn' ← match queue' with
      | [] => pure NTFN.IdleNtfn
      | _ => pure (NTFN.set_ntfnQueue (Notification.ntfnObj ntfn) queue')
    setNotification ntfnPtr ({ ntfn with ntfnObj := ntfn' })

And the first refinement theorem, connecting it to the abstract spec. Its statement mirrors l4v's cancelSignal_corres; the proof uses only Lean's standard axioms, plus a structure that names every l4v lemma it borrows.

theorem cancelSignal_corres (H : CancelSignalAssumptions) (t ntfn : ObjRef) :
    corres dc
      (fun s => invs s ∧ st_tcb_at (· = .BlockedOnNotification ntfn) t s)
      (fun s => invs' s ∧ st_tcb_at' (· = .BlockedOnNotification (toPtr ntfn)) (toPtr t) s)
      (Sel4Lean.Abstract.cancel_signal t ntfn)
      (cancelSignal (toPtr t) (toPtr ntfn))

One surprise from this stage: Lean's do notation compiles let x ← match … into a hidden join point, so our wp needed a rule for something that does not exist in the source text. Small things like that are everywhere when you port a proof culture, not just proofs.

C5The tempting shortcut

Why re-prove anything? Isabelle proofs can in principle be exported. There is a route from Isabelle through the Dedukti/Lambdapi proof format into Lean, and we tried it. It worked end to end: Isabelle's own proofs of the HOL, Orderings and Groups theories came out the other side, and the Lean kernel checked 8.5 MB of them in 245 seconds.

Then the bad news. The exported theorems speak HOL's bool, not Lean's Prop, so they are hard to use from ordinary Lean. And proof terms reached a gigabyte before even finishing HOL's standard library, long before any seL4 content. So we made the decision that shaped everything after: re-prove in Lean, following l4v's proof structure, with AI help, and keep the export route as a cross-check.

Walk: the whole executable spec

Re-proving means the thing being proved has to exist in Lean first. So the walk stage was about translating l4v's entire RISCV64 Haskell model: 62 modules, every data type of the kernel state, every kernel operation.

The translator grew a lot. It learned Haskell fixity, guards, records, scoping, mutual recursion and module imports. Along the way it produced bugs that compiled, which are the scariest kind:

• Multi-clause guards were silently dropped, so f x | c = a | otherwise = b became a.
• 58 non-recursive functions were marked partial, which hides their bodies from proofs.
• Hardware constants were stubbed to zero, so pageBits evaluated to 0.

The fix for "compiles but wrong" was to run both sides. We evaluated pure functions in l4v's Haskell model with GHC and in our Lean with #eval, on the same seeded inputs. The first run had 24 disagreements and 88 cases that would not run at all. Every root cause was a translator bug. After fixing them, 60 of 60 functions agreed.

That felt like a finish line. It wasn't.

The twist: the Haskell is not the spec

When I looked closer at how l4v builds its Isabelle executable spec, I found skeleton files. Each one pulls in Haskell definitions with lines like #INCLUDE_HASKELL file … NOT a b c and writes its own Isabelle in place of the excluded ones. The proofs are about that Isabelle, not about the Haskell. Counting every directive gave a number I did not expect:

105 Haskell definitions that l4v replaces by hand, plus 15 Haskell modules that are not in the verified spec at all.

So matching GHC was the wrong target. My push at this point was simple: make the Lean interchangeable with Isabelle, and validate the test gates against real l4v artifacts. Claude built a gate that runs a session on top of l4v's own compiled ExecSpec heap. It lists every constant the spec defines and asks Isabelle itself to evaluate our test cases. Lean has to give the same answer.

The gate immediately found real differences. Several had compiled fine, and some had even passed the GHC test:

The last row is subtle and I love it. Where l4v leaves something unspecified, a Lean definition with a concrete body would let you prove things in Lean that you cannot prove in Isabelle. So the gate checks specification strength too: anything l4v declares but never defines must be opaque in Lean.

Where the gate stands

The five functions not fully checked hit Isabelle's evaluator limits (large natural-number powers, an enum conversion, an out-of-range list index), not Lean disagreements.

The value gate was a small adventure of its own. The first version ran out of Isabelle's 32-bit heap. Next it ran into datatype internals, which unfold into the datatype package's raw representation. Then it hit simp rules that stay local to l4v's Arch context. The version that works runs each batch of ten cases in its own Isabelle process on top of the l4v heap, six at a time, and evaluates by alternating l4v's own definitions with simplification.

What it cost

This was the actual question, so here are the measured numbers, taken from the session transcript and the git history:

For that, the specification and infrastructure layer is ported, and it is checked against l4v itself rather than against my reading of l4v. The notes, logs and gate outputs behind every number are in the repo, under notes/ and artifacts/.

What is not done is the bulk. Lean has 78 lemmas. The RISCV64 chain has about 14,000, plus the library lemmas they lean on. The C side, which needs a C semantics and parser in Lean, has not started, and the abstract spec (about 22,000 lines of Isabelle) is still to be translated.

Scoping the rest

The estimate below rests on one uncalibrated assumption: 5,000 to 20,000 output tokens per ported lemma, including compile-and-fix loops.

With 20 to 50 agents working in parallel, the throughput floor is a few weeks of wall-clock time. With the C toolchain, rework and human review, two to six months is more realistic. For scale, the original l4v functional-correctness effort is usually cited at around 20 person-years. Even the high end here is a different order of magnitude, if the per-lemma assumption holds.

The cheapest way to make this estimate honest is to measure it: port one medium AInvs theory, a couple of hundred lemmas, end to end, and count tokens and retries per lemma. That is the next step.

What I learned with a beginner's mind

The original work is the asset. Every good decision in this project leaned on something the seL4 team built: their Docker image, their translator conventions, their skeleton files, their compiled Isabelle heap. Porting is not starting over. It is standing on a very tall pile of careful human work and asking the machine to carry it across.

"Compiles" means very little. Almost every interesting bug in this project type-checked. The progress came from gates with teeth: run both sides, compare, and make the reference the thing that was actually proved.

The spec is a negotiated object. I thought "the seL4 spec" was a fixed thing. It is a Haskell model, plus 105 hand-written replacements, plus configuration files, plus deliberate gaps. A faithful port has to respect all four, including the gaps.

The AI pair changed the economics of patience. Claude Opus 5.5 did the long, unglamorous loop: write the translator, run the sweep, read the Lean errors, fix, rerun, commit, update the notes, and do it again at 3 a.m. It caught its own bugs when the gates said so, including one in a proof-relevant instance it had written itself. My job was the part that needed judgment: choose the stages, decide to re-prove, and insist that the reference be l4v's own artifacts.

Lean could broaden the audience. I can't prove this yet. But a Lean seL4 spec that is name-for-name and value-for-value interchangeable with the Isabelle one is something a Lean programmer can open, run with #eval, and start reasoning about on day one. That seems like a real on-ramp for a kernel this good.

Ten years ago, a question like "could we port seL4's proofs to another prover?" meant a grant proposal and a team. This week it meant a weekend, a cloud box and a conversation, and the answer for the foundation is yes. The proofs are the mountain still ahead. What a time to be alive.