Could no amount of formal analysis, type/rule checking prevent it's exploitation? How about a fully verified kernel such as SEL4 ?
According to mathematician Kurt Gödel's incompleteness theorems:
The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "effective procedure" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the natural numbers (arithmetic). For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that such a system cannot demonstrate its own consistency.
Gödel's theorums, in simple terms, say that any sufficiently complex system (non-trivial) cannot prove that it is without flaws.
Software runs on top of hardware, which is also likely to have errors. Even correctly functioning software that encounters a bug at the hardware level will then be classified as failing.