A quick search for "verified bpf compiler" found this: https://github.com/uw-unsat/jitterbug https://github.com/uw-unsat/jitterbug A "direct" correctness proof

A quick search for "verified bpf compiler" found this: https://github.com/uw-unsat/jitterbug https://github.com/uw-unsat/jitterbug A "direct" correctness proof of a BPF compiler written in C would be hard because C is hard to reason about. If you pulled it off, you could do this verification before compiling the kernel. It would certainly be easier to implement an "indirect" approach using translation validation, i.e., taking the code generated by the compiler and checking that it is semantically equivalent to the input BPF code. The problem with this is that this would need to be done at run time, i.e., you would add a lot of verification time when the user is already waiting for the BPF program to run. Overall: Yes, this is a good candidate, and people are on it.