Deductive reasoning à la Hoare logic is a popular foundation for modern program verification tools. The majority of these verification systems consider properties of indvidual executions, but many interesting program properties like observational equivalence, noninterference, co-termination, monotonicity, and idempotency involve reasoning about_multiple_ program executions. Several techniques have been developed to verify these kinds of relational properties, typically taking the form of either bespoke relational program logics or reduction of relational verification problems to verification of equivalent single-execution product programs. Regardless of the underlying approach, the effectiveness of both techniques depends on finding a proper alignment for the programs. An alignment puts subparts of the original programs into correspondence so that their similarities can be exploited by the verifier to, for example, find simplified loop invariants. Existing approaches to product program verification do not posit algorithmic techniques for constructing products, as finding desirable alignments requires efficient representation and exploration of the space of candidate alignments, including consideration for program transformations (e.g., loop unrolling) to make such alignments feasible. We propose an approach using e-graphs and equality saturation along with rewriting rules from an algebra of program alignments to efficiently represent and extract verifiable product programs. We present a prototype tool called KestRel which automatically constructs product C programs using this approach, along with preliminary experimental data which showcase the potential of our approach.