There's a second reason I think that they're phrasing it as "long term" computation, but their requirements discuss formal verification in some detail. It's tr

There's a second reason I think that they're phrasing it as "long term" computation, but their requirements discuss formal verification in some detail. It's true that building up a large bank of formal proofs could take large amounts of super computer time -- eg, dealing with something the size of drivers or a kernel -- and that with the current upgrade cycle and manner that hardware is specified, this might not be practical. However, if you developed a framework for your proofs that generated a proof generator which generated a final proof easily when given a schematic of the hardware to execute the algorithm and made such a framework general enough that you can use it to make schematics when you upgrade your hardware, then your time spent making the proof generator isn't wasted every hardware cycle. Once your proof system isn't reset every time you upgrade hardware, it begins to make more sense to develop things like your firewall, IDS, routing, crypto, etc code in terms of formally verified systems (that generate machine specific code in automatic ways). When you combine this project with other DARPA cybersecurity projects, it becomes clear that DARPA is looking to transition key infrastructure in to formally verified, machine upgradable systems in preparation of high-speed automated cyberwarfare. (Think the difference between HFT and a guy on the E-trade website applied to scanning software for vulnerabilities and generating things like Flame automatically.) tl;dr: DARPA's plan for the next 10-20 years seems to be that they're afraid of AIs beating them at cyberwar, and this is a piece of their solution.