[red_admiral]

It solves the halting problem by not being Turing complete. I presume each eBPF runs in a context with bounded memory, requested up front, for one thing; it also disallows jumps unless you can prove the code still halts.