Kernel formal methods mailing list?

[James Morris <jmorris@namei.org>]

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>