BPF and formal verification
Intro to BPF (specifically the OpenBSD flavor, though without loss of generality) and verification.
> BPF is also a fantastic target for formal verification because it can only jump forward. This avoids the halting problem – BPF programs have a finite set of possible states and must terminate. We can therefore model BPF and analyze its programs completely rather than resorting to heuristics that give false positives.