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.