Den indledende fase af den amerikanske hærs forsvarsanalyseprojekt agenturets (DARPA) publikumsoprettede formelle verifikationseksperiment (CSFV), der blev lanceret i 2013. Forsøget blev oprettet for at bekæmpe de dyre, tidskrævende faldgruber af traditionelle kodeverifikationsmetoder.
Drevet af hypotesen om, at "stort antal ikke-eksperter kan udføre formel kontrol hurtigere og mere omkostningseffektivt end konventionelle processer", har DARPA designet CSFV-programmet til at kontrollere store partier kode for nøjagtighed ved brug af browserbaserede videospil.
På onsdag udråbte DARPA programmet succes og annoncerede tilføjelsen af fem nye spil til sin eksisterende lineup. Fra DARPA bloggen:
Disse [2013] spil oversatte aktørers handlinger i programannoteringer og assisterede formelle verifikationseksperter ved at generere matematiske beviser for at verificere manglen på vigtige klasser af fejl i "C" og "Java" programmeringssprog. En indledende analyse viser, at ikke-eksperter, der spiller CSFV-spil, genererede hundredtusindvis af annoteringer.
De nye titler omfatter puslespillere Dynamakr, Paradoks, og Binær fission, "science game" Ghost Map Hyperspace, og fantasy sim Monster Bevis. Alle DARPAs CSFV-spil, herunder dem fra 2013-projektfasen, er tilgængelige online på Verigames. Spillere skal være 18 år eller ældre for at deltage.