It's less a matter of having a proof (or not having one), and more a matter of having a sufficiently short proof (or simple by other criteria) that your adversary will find it before they give up.

In general, I think any algorithm with behavior X and a proof has another algorithm with identical behavior and no proof of it. But here we're interested in algorithms that are chosen (by their makers) to be deliberately easy to prove things about.

What are the odds that a system that reliably defects will not have a proof that it defects,

It won't want others to prove it will defect. So if others cooperate when unable to prove either way, then it can always construct itself to make it unproveable that it defects.

that a system that cooperates if it is cooperated with will have no proof.

It will want to have a proof. Here the question is, how good the adversary is at finding proofs in practice. Which is what I asked elsewhere, and I would really like to have an answer.

However, perhaps the system knows its own proof (or its designer knew it). Then it can just write out that proof at the start of its source code where the adversary is sure to see it.