[Beltiras]

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

[jdefr89]

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

[hga]

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