How do you even begin to define what correctness means for the transformations if you have no formalized model of the thing you're transforming into?

This is another reason we are being careful with the correctness claim. The closest project I know right now that comes close to a formalized model of C++ is the BRiCk project:

https://skylabsai.github.io/BRiCk/index.html

https://github.com/SkyLabsAI/BRiCk