The same unsafe constructs can cause memory corruption in the verification tool and lead to a behavior where the wrong decisions are taken.
So the fact that many C verification tools are written in C itself does not proof anything about how safe the language could be.
For me personally C could be much better if:
- There was no automatic decay from arrays into pointers (call an explicit operation to do so, like &a[0])
- There was a proper string type available
- Arrays were bound checked (with optional disabling of bound checking, like many other languages offer)
