I think that there is a strong limit to that: if you don't understand the proofs, you're going to have a hard time understanding when the model explains to you why your code is not correct.
In most cases I expect saying "<this> assertion fires with <this> input" is enough to be useful. Or "I can't prove <this> assertion doesn't fire, but I don't have a counter example either". Assertion used broadly to include things like rules for avoiding undefined behavior.
Better explanations would be nice of course, but not obviously practical. I wouldn't actually trust the AIs reasoning much in the first place, only that it can't trick the proof checking tool.
Better explanations would be nice of course, but not obviously practical. I wouldn't actually trust the AIs reasoning much in the first place, only that it can't trick the proof checking tool.