Kernel formal methods mailing list?

Kernel formal methods mailing list?

[James Morris]

Hi Folks,

I've tried to include folk who are known to be working on formal 
verification for the Linux kernel. Apologies if I've missed anyone and 
please forward as appropriate.

Several Linux kernel developers & researchers have been experimenting 
with formal methods in recent times, I think largely due to the potential 
of LLMs to lower some of the costs and barriers to entry.

Examples I'm aware of include a presentation by Corinn Tiffany at LPC on 
her work with XArray [1], and Christian Brauner's linux-formal repo [2].

I've been experimenting with formal verification as part of a hypervisor 
research project [3] (which is admittedly not the kernel).

I'm interested in learning from what others are doing in this area, and 
sharing potentially useful findings, especially in terms of identifying 
_practical_ approaches for verification of low-level systems code.

I suspect there's a lot that can be done on smaller scale, well-defined 
projects, by developers who don't necessarily have specific expertise in 
formal methods, but have deep expertise in the target subsystem.

Thoughts? Would it be worth setting up a mailing list?


[1] https://lpc.events/event/20/contributions/2540/
[2] https://github.com/brauner/linux-formal
[3] https://github.com/orgs/beryllium-project/repositories (WIP review snapshot)


-- 
James Morris
<jmorris@namei.org>

Re: Kernel formal methods mailing list?

[Natalie Klaus]

[-- Attachment #1.1: Type: text/plain, Size: 1514 bytes --]

Hi James,

Adding Palina Tolmach (CTO, Runtime Verification) and Andrey Klaus
to Cc.

Great idea, +1 for the mailing list.

We have a prototype deterministic (non-LLM) C to Lean 4 translator
aimed at low-level C, with the Linux kernel as the main target,
including threads and mutexes. Andrey Klaus is working on it. The
generated Lean stays close to the source and is executable. Coverage
of real-world C is still limited. Proving the translation equivalent
to the C source should be possible, but is a separate research effort.

We also use a C -> Rust -> Aeneas -> Lean 4 path, checked against the
C by differential fuzzing. We tried it on UVC [1], Binder [2] and the
userns ID mapping [3]; the last one produced the uid_map range patch
Christian applied. On the io_uring cBPF filter validator [4] it found
a CONNECT filter bypass, fixed in aa5d5f8e5023 [5].

Looking forward to the list.

[1] https://github.com/runtimeverification/kernel-c-to-rust-spike
    https://runtimeverification.com/blog/hardening-linux-c-code-a-rewrite-and-verify-loop
[2] https://github.com/runtimeverification/kernel-rust-verification-spike
[3] https://github.com/runtimeverification/linux-isolation-spike
[4] https://github.com/runtimeverification/linux-cbpf-spike
[5] https://lore.kernel.org/io-uring/20261009133807.730724-1-natalie.klaus@runtimeverification.com/
[6] https://github.com/runtimeverification/kernel-rust-coverage-map
[7] https://arxiv.org/abs/2605.30106 (AIMACS / CAV 2026)

Natasha

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 343 bytes --]

Re: Kernel formal methods mailing list?

[Greg KH]

On Tue, Nov 03, 2026 at 03:59:52PM -0800, James Morris wrote:
> Hi Folks,
> 
> I've tried to include folk who are known to be working on formal 
> verification for the Linux kernel. Apologies if I've missed anyone and 
> please forward as appropriate.
> 
> Several Linux kernel developers & researchers have been experimenting 
> with formal methods in recent times, I think largely due to the potential 
> of LLMs to lower some of the costs and barriers to entry.
> 
> Examples I'm aware of include a presentation by Corinn Tiffany at LPC on 
> her work with XArray [1], and Christian Brauner's linux-formal repo [2].
> 
> I've been experimenting with formal verification as part of a hypervisor 
> research project [3] (which is admittedly not the kernel).
> 
> I'm interested in learning from what others are doing in this area, and 
> sharing potentially useful findings, especially in terms of identifying 
> _practical_ approaches for verification of low-level systems code.
> 
> I suspect there's a lot that can be done on smaller scale, well-defined 
> projects, by developers who don't necessarily have specific expertise in 
> formal methods, but have deep expertise in the target subsystem.
> 
> Thoughts? Would it be worth setting up a mailing list?

Sure, what's one more list for us to be on :)

Re: Kernel formal methods mailing list?

[Miguel Ojeda]

On Wed, Nov 4, 2026 at 1:00 AM James Morris <jmorris@namei.org> wrote:
>
> I'm interested in learning from what others are doing in this area, and
> sharing potentially useful findings, especially in terms of identifying
> _practical_ approaches for verification of low-level systems code.

I have been trying Aeneas (Rust -> Lean 4 in particular), which still
needs work for low-level/kernel/`unsafe` development (which is coming,
from what I am told), but it can already be useful for a subset of
safe Rust (and ideally single-crate).

I agree there are things that subsystems would probably start doing
"locally" first, i.e. picking different approaches depending on their
needs.

And, yeah, LLMs definitely are playing a role in making this way more
cost-effective and thus popular :)

Cheers,
Miguel

Re: Kernel formal methods mailing list?

[Paul E. McKenney]

On Tue, Nov 03, 2026 at 03:59:52PM -0800, James Morris wrote:
> Hi Folks,
> 
> I've tried to include folk who are known to be working on formal 
> verification for the Linux kernel. Apologies if I've missed anyone and 
> please forward as appropriate.
> 
> Several Linux kernel developers & researchers have been experimenting 
> with formal methods in recent times, I think largely due to the potential 
> of LLMs to lower some of the costs and barriers to entry.
> 
> Examples I'm aware of include a presentation by Corinn Tiffany at LPC on 
> her work with XArray [1], and Christian Brauner's linux-formal repo [2].
> 
> I've been experimenting with formal verification as part of a hypervisor 
> research project [3] (which is admittedly not the kernel).
> 
> I'm interested in learning from what others are doing in this area, and 
> sharing potentially useful findings, especially in terms of identifying 
> _practical_ approaches for verification of low-level systems code.
> 
> I suspect there's a lot that can be done on smaller scale, well-defined 
> projects, by developers who don't necessarily have specific expertise in 
> formal methods, but have deep expertise in the target subsystem.
> 
> Thoughts? Would it be worth setting up a mailing list?

We do have (low-traffic) lkmm@lists.linux.dev, though that was intended to
be specific to the Linux kernel memory model and its formal-verification
tooling.

							Thanx, Paul

> [1] https://lpc.events/event/20/contributions/2540/
> [2] https://github.com/brauner/linux-formal
> [3] https://github.com/orgs/beryllium-project/repositories (WIP review snapshot)
> 
> 
> -- 
> James Morris
> <jmorris@namei.org>
> 

Re: Kernel formal methods mailing list?

[James Morris]

On Wed, 4 Nov 2026, Paul E. McKenney wrote:

> > Thoughts? Would it be worth setting up a mailing list?
> 
> We do have (low-traffic) lkmm@lists.linux.dev, though that was intended to
> be specific to the Linux kernel memory model and its formal-verification
> tooling.

That's a possibility. Would the mm folk there would want to keep it domain-focused?


-- 
James Morris
<jmorris@namei.org>