I considering it now. Aside from correctness verification, the main reason we'd use a limited language for packet inspection is in case the policy is malicious. How often is that the case?

For most people, they trust most or all of the code running on their machine. They certainly trust their firewall policy to not be malware. If you already trust it, using a better, safe language might be helpful. In many cases, eBPF will be fine.

This isn't the first time this has been done. SPIN was an operating system in Modula-3 that allowed type-safe linking of code into the kernel, balancing safety and performance.