Re: Kernel formal methods mailing list?

[Miguel Ojeda]

On Wed, Nov 4, 2026 at 1:00 AM James Morris <jmorris@xxxxxxxxx> 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