Work on equality saturation (EqSat) has established a wide breadth of applications across domains, including automated theorem proving, program synthesis, and compiler optimization. While EqSat and its underlying e-graph data structure contribute to the foundations of many automated theorem provers, attempts to leverage EqSat in domains that require checkable proofs, most notably interactive theorem provers like Rocq and Lean, have only recently seen success. Two challenges are responsible for the limitations of past work: most obviously, the need to generate proofs that certify the results of e-graph queries, but also the related difficulty of managing encodings across tool boundaries, especially encoding terms of expressive programming languages in the e-graph.
We present a solution to both these problems: the first verified, object language-generic EqSat procedure implemented in Rocq, following the structure of the egglog fixpoint reasoning system. Because we prove our procedure sound, it does not need to generate certificates. Instead, users can simply apply the soundness theorem to a proof goal and run the resulting computation. The input to our procedure is specified in the Pyrosome framework, which allows users to write language specifications and equations as inference rules, and we handle the encoding details internally. To demonstrate the benefits of verified EqSat, we perform type inference, type checking, and equivalence checking on arbitrary Pyrosome languages using our e-graphs, which we combine into a language-agnostic methodology for automatically verifying translation passes in a compiler pipeline. Our case studies include the first demonstration compiler fully automatically verified using language-agnostic procedures.