While this isn't optimization, is there any LLM systems that create "provably correct" transformations yet?

I have used ChatGPT on some fairly awful code, asking it to add comments, rename variables and functions, etc. I find the outputs useful, but a couple of times it's broken the code. I imagine for many (not all) languages, you could ask the LLM to produce suggested changes, then use a code-rewriting tool to apply them in a way you could be 100% sure they weren't going to change the behaviour of the progrma.