Paper Accepted by eBPF 2026
Our paper titled “Formal Specification of Linux eBPF Instruction Set Architecture in Sail” by Yazhou Tang, Shenghao Yuan, Jean-Pierre Talpin (INRIA), and Mingshuai Chen has been accepted for presentation at eBPF 2026 – the 4th Workshop on eBPF and Kernel Extensions co-located with ACM SOSP 2026, in Prague, Czech Republic. This short paper presents a Sail formalization of the Linux eBPF ISA that covers all sequential instructions and serves as a single source for generating both a human-readable specification and executable Rocq semantics.