Paper Accepted by OOPSLA 2026

Our paper titled “Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications” by Shenghao Yuan, Yazhou Tang, Tianci Cao, Frédéric Besson (INRIA), Jean-Pierre Talpin (INRIA) and Mingshuai Chen has been accepted for publication at OOPSLA 2026, in Oakland, California, United States, as part of the Proceedings of the ACM on Programming Languages (PACMPL). This paper presents a mechanized, fully executable small-step semantics in Rocq for all the 160 sequential in-kernel instructions of the Linux eBPF instruction set architecture. Leveraging this semantics, we verify the soundness of the Linux verifier’s bit-level abstract domain, uncover previously unknown kernel bugs, and develop verifier optimizations, all of which have been upstreamed to the Linux kernel.