The Extended Berkeley Packet Filter (eBPF) subsystem within an operating system’s kernel enables userspace programs to extend kernel functionality dynamically. Because of the security risks arising from runtime modification of the OS, eBPF requires all programs to be verified before deploying them inside the kernel. Existing approaches to eBPF verification are monolithic, requiring their entire analysis to be done in a secure environment, resulting in the need for extensive trusted codebases. To reduce the size and complexity of the trusted codebase, we propose a type-based verification approach that automatically infers proof certificates in userspace, while only the proof-checking component needs to be deployed in a secure environment. Moreover, compared to previous techniques, our type system enhances the debuggability of the programs for users through ergonomic type annotations when verification fails. We implemented our type inference algorithm in a tool called VeRefine and evaluated it against an existing eBPF verifier, Prevail. VeRefine outperformed Prevail on most of the industrial benchmarks.