I considered saying that proofs are verifiable by definition. I mean a proof in formal logic. The point of formal logic is that it is computable (even fast) to verify it. The point, which matches the common usage, is that it is convincing. You can't prove anything about arbitrary code; these algorithms are not guaranteed to understand the opponent. But it's interesting that sometimes they do succeed in proving things about their opponents.