Yes; see also the vellvm project, which develops proofs of a number of the equivalences LLVM uses: https://www.cis.upenn.edu/~stevez/vellvm/

The equivalences (between equivalent programs) correspond to specific rewrite rules. Equality saturation allows the consolidation of many such rules into a single optimization pass, without complicated ordering and assumptions, instead of arbitrary grouping that is likely to neglect opportunities.