Is there a tool for verifying that a statement like

day == 28 && leapYear || day == 29 && !leapYear

is equivalent to

day == if(leapYear) 28 else 29

?

You can use a SMT solver (Z3 is one of the best) to perform such kind of reasoning

Perhaps property based testing could help https://kotest.io/docs/proptest/property-based-testing.html