[helltone]

Program equivalence is undecidable, in general, but also in practice (in my experience) most interesting cases quickly escalate to require an unreasonable amount of compute. Personally, I think it is easier to produce correct-by-construction decompilation by applying sequences of known-correct transformations, rather than trying to reconstruct correctness a posteriori. So perhaps the LLM could produce such sequence of transforms rather than outputting the final decompiled program only.

[fulafel]

Yes, something like this, the intermediate verified steps wouldn't have to be shown to the user.