This paper describes our experience deploying automated verification techniques for proving the correctness of value tracking components of the eBPF verifier in the Linux Kernel over the last four years. The eBPF verifier uses abstract interpretation with multiple abstract domains for value tracking. The eBPF verifier uses non-standard approaches for refining the results from multiple abstract domains, which necessitated us to design new techniques to show their correctness. During this process, we also discovered that some of the abstract operators are unsound in isolation. The unsoundness of these operators are eventually corrected by a shared refinement operator. The presence of intermediate “latent” unsound abstract operators makes the task of verification harder. We describe our patches to the Linux kernel, which have been upstreamed, that fix these latent errors and make the abstract operators correct in isolation, which enables faster automated verification.