There was an interesting research article on verifying equivalences between Spark programs at this year’s conference on Computer Aided Verification.
Perhaps unsurprisingly, they seem to be leveraging the well known relationship between relational queries and first order logic. I hope to find some time to do a more in-depth review some time, but this week is busy with deadlines.