Re: Kernel formal methods mailing list?

[Greg KH <greg@kroah.com>]

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 :)