We present Leapfrog, a Coq-based framework for verifying the equivalence of network protocol parsers. Our approach is based on an automata model of P4 parsers, and an algorithm for symbolically computing bisimulations modulo ``leaps'' that greatly simplifies the symbolic representation. Proofs are powered by a Coq plugin that uses an off-the-shelf SMT solver to decide the validity of first-order entailments, resulting in a fully automatic, push-button tool for verifying equivalence. We mechanically prove the core metatheory that underpins our approach, including the key transformations, along with several optimizations. We evaluate Leapfrog on a range of practical case studies, all of which require minimal configuration and no manual proof. Our largest case study uses Leapfrog to perform translation validation for a third-party compiler from automata to hardware pipelines. Overall, Leapfrog represents a step towards a world where all parsers for critical network infrastructure are verified. It also suggests directions for follow-on efforts, such as verifying relational properties involving security.