Kevin Hartnett, Senior Writer at Quanta Magazine, expounds on the notion of formal code verification when used to provide assurance of attack-proof code... Similar to unsinkable ocean liners? Or, is it only a matter of time before a successful attack is mounted thereupon? Is attack-proof code provable utilizing proofs (as in mathematical proofs)? You be the judge.

'“They were not able to break out and disrupt the operation in any way,” said Kathleen Fisher, a professor of computer science at Tufts University and the founding program manager of the High-Assurance Cyber Military Systems (HACMS) project. “That result made all of DARPA stand up and say, oh my goodness, we can actually use this technology in systems we care about.”' - via Kevin Hartnett, Senior Writer at Quanta Magazine