I have such a request. I recently came across this article: Trent Moore, DARPA DEVELOPING NEW COMPUTER CODE THAT IS EFFECTIVELY HACK-PROOF.
This reports an assertion by DARPA that the process of “formal verification” had allowed it to develop code that could not be hacked. Since I had always understood that this was not possible (as opposed to, say, very difficult/expensive to achieve) the report strikes me as very significant — if true. Anyone out there with cyber-chops willing to share with me thoughts on its accuracy? Send responses to: firstname.lastname@example.org. Thanks in advance!