Den inledande fasen av den amerikanska arméns försvarsforskningsprojektbyrås (DARPA) publikationssökande formell verifiering (CSFV) -experiment lanserades 2013. Experimentet skapades för att bekämpa de dyra, tidskrävande fallgroparna med traditionella kodverifieringsmetoder.
Med hjälp av hypotesen att "stort antal icke-experter kan genomföra formell verifikation snabbare och mer kostnadseffektivt än konventionella processer", utformade DARPA CSFV-programmet för att kontrollera stora partier kod för noggrannhet med hjälp av webbaserade videospel.
På onsdagen utropade DARPA programmet en succé och tillkännagav tillägget av fem nya spel till sin befintliga lineup. Från DARPA-bloggen:
Dessa [2013] -spel omvandlade aktörers handlingar till programannoteringar och assisterade formella verifieringsexperter för att generera matematiska bevis för att verifiera avsaknaden av viktiga klasser av brister i "C" och "Java" programmeringsspråk. En inledande analys indikerar att icke-experter som spelar CSFV-spel genererade hundratusentals annoteringar.
De nya titlarna inkluderar pussel Dynamakr, Paradox, och Binär fission, "science game" Ghost Map Hyperspace, och fantasy sim Monster Bevis. Alla DARPAs CSFV-spel, inklusive dem från 2013-projektfasen, finns tillgängliga på Verigames online. Spelare måste vara 18 år eller äldre att delta.