[$] Even more formal verification for BPF

BPF offers useful safety guarantees, but Kumar Kartikeya Dwivedi wants BPFprograms to be even safer. At the 2026Linux Storage, Filesystem,Memory-Management, and BPF Summit, he led a session(slides)discussing the possibilityof adding domain-specific invariants to BPF programs. It was not a discussionintended to lead to the implementation of any particular kernel feature, butrather an overview of why additional formal verification might be needed, andhow it could work with the existing BPF ecosystem.