Formal verification doesn't mean your design can't be flawed in other ways that your theorem prover can't identify.
See also: Software AES with cache-timing information leaks.
See also: Software AES with cache-timing information leaks.
FTA:
“We’re not claiming we’re going to prove an entire system is correct, 100 percent reliable in every bit, down to the circuit level,” Wing said. “That’s ridiculous to make those claims. We are much more clear about what we can and cannot do.”
Hacker-proof is just going to hurt branding of formal methods the second a hacker takes out a high-assurance system. Whereas, the formal methods and high-assurance literature written by anyone with sense acknowledges plenty of assumptions that might be targeted plus just human error. Even the people they quote in the article don't say it's hacker-proof!
https://www.usenix.org/system/files/conference/usenixsecurit...
http://www-bcf.usc.edu/~wang626/pubDOC/EldibWS14_TOSEM.pdf
It's analog and RF side channels that's going to screw them. DOD et al did decades of cat and mouse games under that with their TEMPEST activities. Open research just getting started. Just waiting for The Flood. :)