He did show that every formal axiomatic system will have statements that can't be proven "from within".

For these, you are left with doing a runtime check.

Yes, that's true, but then possibly we are talking at cross-purposes; when I said "numerous holes discovered in various implementations of the basic JVM type checking", I didn't mean things that needed to be checked at runtime; I meant bugs that permitted violations of the JVM's security guarantees. However difficult it may be to avoid such things at a social level, certainly there is no mathematical reason that they must happen.