Kernel Rust verification spike: Binder → Lean 4

Can the Linux kernel's Rust Binder driver be verified post hoc, through the Charon/Aeneas toolchain (Rust → LLBC → Lean 4)? Target property, from the Binder maintainer: for all inputs from userspace, the code must not panic.

Status.

• Charon extracts the BinderObject deserializer (drivers/android/binder/allocation.rs, v7.2-rc2) with zero changes to the parsing logic. Only the kernel environment (kernel crate, bindgen'd UAPI, userspace reader) is stubbed, marked // SPIKE-STUB in the source. Details: CHARON-REPORT.md.
• Aeneas rejects the union type-punning at the core of the deserializer, so the parsing functions get no Lean at all. Upstream issue: AeneasVerif/aeneas#1199
• The union-free validators translate, and no-panic is proved for three of them (size_check unconditionally). Theorems: lean/NoPanic.lean. Details: AENEAS-REPORT.md.

Layout

• src/ — the extracted crate, parsing logic byte-for-byte from the kernel
• reduced/ — union-free subset that Aeneas accepts
• lean/ — generated Lean 4 code + no-panic theorems (Lake project)
• llbc/ — Charon artifacts
• CHARON-REPORT.md, AENEAS-REPORT.md — full results for each stage

Reproduce

# Charon at commit 909ff09a (v0.1.220, the version Aeneas pins), Aeneas c2015b86
git clone https://github.com/AeneasVerif/charon.git ~/charon
cd ~/charon && git checkout 909ff09a && make build-charon-rust

cargo test                                        # 3/3
charon cargo --preset=aeneas                      # full crate -> llbc; Aeneas then fails on unions
cd reduced && charon cargo --preset=aeneas        # union-free crate -> translates
aeneas -backend lean llbc/spike_binder_reduced-charon-909ff09a-v0.1.220.llbc -dest lean/
cd lean && lake build                             # typechecks generated code + theorems

Kernel v7.2-rc2, Lean/mathlib v4.31.0, stable rustc 1.94.0. Aeneas requires --preset=aeneas at extraction time.

Next

• Union-free re-modelling of BinderObject ([u8; 40] + typed accessors), type-pun invariants as explicit Lean propositions — the path to no-panic on parse_one
• Coverage map: the rest of the kernel's Rust through both pipeline stages

Who

Runtime Verification, Inc. Issues welcome, or the Rust-for-Linux Zulip thread.