Not yet. But there may be in the future. Many things proved impossible have shown to be possible in the past.

Gödel's Incompleteness Theorem might be abstractable to this. Any system so inaccessible as to be unhackable might be functionally impaired beyond usefulness.

Godel's theorem is great for claims like this. Have they proved that the "theorem proving" software has no mistakes?

There's this: http://proof-technologies.com/holzero/index.html and I see some other things that I interpret as moving in that direction.