[$] Formally verifying the BPF verifier

The BPF verifier is an increasingly complex and security-critical piece of code.When the kinds of people who are apt to work on BPF see a situation like that,they naturally question whether it's possible to use formal verification toensure that the implementation of the code in question is correct. SantoshNagarakatte led the first of two extra-long sessions in the BPF trackof the 2025 Linux Storage, Filesystem, Memory Management, and BPF Summitabout his team's work formally verifying the BPF verifier with acustom tool calledAgni.