Verifying Linux's Rust Code: From Binder To Lean 4

I did the math today: for twenty years now, Linux has been my one and only operating system. The reason for this loyalty is simple: nothing breaks, everything works, I have never had to deal with a virus. It could hardly be better. I change distributions about once a decade. There was SUSE, then Ubuntu. The one constant underneath was the kernel. Twenty years ago it had zero lines of Rust. Today Rust is about 0.2 percent of it. That sounds negligible until you look at where that code sits.

The Linux kernel now contains over 90,000 lines of Rust. Some of it parses data that arrives from outside the trust boundary: ioctl arguments from userspace, firmware blobs from devices, transaction buffers from arbitrary apps. Parsing untrusted bytes is historically where kernels get hurt. We set out to check whether this code can be formally verified, post hoc, without modifying it, with proofs checked by a machine.

Short answer: yes, with caveats we'll be explicit about. This post describes the first proven theorems, the map of what's reachable, and what broke along the way.

The first target: Binder

Binder is Android's IPC mechanism. Every Android phone and tablet uses it, over three billion devices. Every app talks to system services through it, so its kernel driver deserializes attacker-controllable bytes all day. The driver was rewritten in Rust and merged into mainline, which eliminates memory-unsafety by construction. Logic bugs remain possible: a reachable panic in the kernel is a denial of service, and incorrect validation is worse. That makes Binder's deserializer a natural first verification target: high value, well-scoped, and its maintainer told us exactly which properties matter.

Asking the maintainers first

Before proving anything, we asked the people who own the code what would be worth proving. In the Rust-for-Linux Zulip, Binder's maintainer named two properties: the code must not panic on any userspace input, and object cleanup must exactly match what was translated. The Rust-for-Linux lead added further questions: does the whole chain work, not just the front end, and can the extraction be maintained over time rather than hard-copied once? The thread is public: Verifying Binder's parsing of userspace input in Lean 4.

The maintainers also named two follow-up targets:

• No-panic for the transaction copy loop. The heavier half of the driver, not yet extracted.
• No sleeping in atomic context. An existing static tool (klint) catches most cases by control-flow analysis, but cannot handle the ones where entering the atomic context depends on a runtime value, such as a try_lock that may or may not succeed. Those cases need reasoning about values, which is what a proof-based approach does natively.

The pipeline

Our goal is always to verify production Rust as written. The pipeline uses Charon and Aeneas, which extract Rust into Lean 4, where properties are stated and proved. Where the toolchain does not yet support a feature, we re-model the affected fragment and pin the re-model to the original with compile-time assertions; the rest of the code goes through unmodified. Proof obligations are discharged with AI provers where possible; every proof is checked by the Lean kernel, so nothing AI-generated is trusted. We've described the pipeline in detail before, in our From Rust source code to mathematical proof blogpost. Nobody should have to rewrite their driver to make it provable; where we do re-model, the assertions keep the model honest.

We've described the same pipeline academically, applied there to zkEVM cryptographic code, in our arXiv paper (accepted at AIMACS/CAV 2026): https://arxiv.org/abs/2605.30106. We utilize the same toolchain and AI-prover workflow, here aimed at the kernel.

What broke

The Charon step was uneventful: the Binder deserializer, with its union type-punning, MaybeUninit, raw pointer casts and unsafe blocks, extracted to ULLBC (Charon's format) with zero changes to the parsing logic. The Aeneas step was not: Aeneas does not support union types, and the deserializer is built on exactly that, a C-style union filled from raw bytes and read through a tag-selected typed view. The failure cascades: no Lean output at all for the parsing core. We filed it upstream (aeneas#1199) and are working with the Aeneas authors to figure out expanded support.

The workaround

With the Aeneas authors we settled on a re-modelling: the union becomes a plain byte array, [u8; 40], and the union's field reads become typed accessor functions reading at fixed offsets. This is what the memory does anyway. Two things keep the re-model honest. Compile-time assertions pin every accessor offset and every size to the real #[repr(C)] layout, checked against the actual kernel structs. And the invariants that unsafe code kept in SAFETY comments (all bytes initialized, tag matches the accessed variant) become explicit Lean propositions, visible and checked, instead of implicit in a translation.

We contributed to Aeneas upstream before, and our default when the toolchain lacks something is to fix it there rather than accumulate local workarounds. The re-model is the interim path while union support lands.

What's proved today

For all byte inputs from userspace, the Binder deserializer returns cleanly: a valid object or EINVAL, never a panic. Machine-checked end-to-end through Rust, Charon, Aeneas, and Lean 4, sorry-free, modulo one opaque axiom about size_of. This is the maintainer's property 1, on the deserializer fragment. Along the way: no-panic theorems for the bounds validators, alignment checks, and every field accessor. Code, theorems, and reports are available in this repo: kernel-rust-verification-spike.

The map: from one driver to the whole tree

One theorem on one driver doesn't tell you whether the approach scales. So we ran all of the kernel's Rust through the extraction stage and published the result: kernel-rust-coverage-map, 92k LOC. There were two interesting findings. Zero failures on language features: everything that compiles, extracts. And 27 of 28 whole-crate failures share a single cause, the unstubbed kernel crate surface. Reaching the rest of the tree is one shared, mechanical cost, not a per-driver research problem. The four highest-value untrusted-input targets in the tree (nova-core's firmware parsers, Binder, DRM, and iov) all carry the same union pattern, so the re-modelling transfers.

What this doesn't prove

The theorem covers the deserializer fragment, not the full transaction path; the cleanup/translate symmetry (the maintainer's property 2) needs the heavier half of the driver extracted and is next. size_of is an opaque axiom in the current extraction. And the proof is about the re-modelled code, pinned to the kernel's layout by assertions; a proof about the union code as written awaits union support in Aeneas.

What's next

Property 2, then the transaction copy loop. Growing the shared kernel-surface model the map calls for. Union support upstream. And more targets from the map's shortlist. If you maintain kernel Rust that parses untrusted input and want to know what a machine-checked property for it would look like, we'd like to hear from you: that question, asked about Binder, is what produced this work.

Acknowledgements

We thank to Alice Ryhl and Miguel Ojeda for pointing us at the properties worth proving and for the questions that shaped this work.