Another way of working around Rice's theorem is to search for methods which catch many bugs, without being complete.

I'd guess that hypothetical AI cybersecurity verification of code would be like that, where there are probably no bugs, but it's not a totally sure thing. But even if you can't have mathematical certainty there are no bugs, that doesn't mean every or most programs verified this way are possible to be exploited.