<p>hey, compiler folks, check this out</p><p>in Project Unnamed we have a way to automatically verify transformations using an SMT solver. we do this by collecting calls to replace-all-uses-with in a staging area, checking it while using the before-after correspondence to make the SMT query more tractable, then applying in bulk</p><p>if the query fails, we print the design with diff markup, which gets highlighted like the below</p><p>the verifier will also tell you which RAUW calls were illegal</p><p>how cool is this?</p>