[vitus]

That's a good point. I should clarify that no such verification is necessary in classic BPF due to the absence of backward jumps -- you can trivially show that the maximum steps executed by a BPF program is 4096, since you'll execute each instruction at most once, and there are at most 4096 instructions.

Meanwhile, the verification that an eBPF program terminates is dependent on the correctness of the verifier, and similarly there's no guarantee that a program with appropriately-bounded complexity will be accepted by the verifier.

To be clear: I'm not trying to throw shade at the verifier; to the contrary, I think it's an impressive piece of software. But there's a difference between being able to prove in one sentence that a program always terminates, and needing to rely on the correctness of some verification software.