The initial phase of the US Army’s Defense Advanced Research Projects Agency’s (DARPA) crowd-sourced formal verification (CSFV) experiment launched in 2013. The experiment was created to combat the expensive, time-consuming pitfalls of traditional code verification methods.
Operating on the hypothesis that “large numbers of non-experts can perform formal verification faster and more cost-effectively than conventional processes,” DARPA designed the CSFV program to check large batches of code for accuracy using browser-based video games.
On Wednesday, DARPA proclaimed the program a success and announced the addition of five new games to its existing lineup. From the DARPA blog:
These [2013] games translated players’ actions into program annotations and assisted formal verification experts in generating mathematical proofs to verify the absence of important classes of flaws in the “C” and “Java” programming languages. An initial analysis indicates that non-experts playing CSFV games generated hundreds of thousands of annotations.
The new titles include puzzlers Dynamakr, Paradox, and Binary Fission, “science game” Ghost Map Hyperspace, and fantasy sim Monster Proof. All of DARPA’s CSFV games, including those from the 2013 project phase, are available online at Verigames. Gamers must be 18 years of age or older to participate.
