There's a subtlety being missed here. Proven termination of BPF programs far predates the adversarial threat model you and the WASM person are thinking about. It was a property of the original 1991 McCanne BPF. It's a safeguard for the programmer against themselves. eBPF shims in all over the place in the kernel; it would not be OK for the guarantee to simply be "there's a worst case maximum cycle budget for programs". eBPF programs are bounded, so they can be installed in hot places in the kernel.

The solved problem you're referring to is a much simpler problem.