Re: Kernel formal methods mailing list?

[Natalie Klaus]

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@xxxxxxxxxxxxxxxxxxxxxxx/
[6] https://github.com/runtimeverification/kernel-rust-coverage-map
[7] https://arxiv.org/abs/2605.30106 (AIMACS / CAV 2026)

Natasha

Attachment: signature.asc
Description: OpenPGP digital signature