An LSFMM+BPF session proposes proving scheduler and XDP invariants with Verus

Sources: LWN report, HN discussion
Summary: An LSFMM+BPF session covered by LWN proposes using Verus to prove invariants about BPF scheduler and XDP programs, because the BPF verifier only guarantees the kernel does not crash. Kumar Kartikeya Dwivedi reports that one or two sched_ext schedulers are kicked out by the watchdog every month at Meta, and that harder cases regress performance without failing outright.
Why it matters: A BPF program that passes the verifier can still make a machine unusable, so the properties that matter operationally are outside what the verifier checks today.