Den første fasen av den amerikanske hærens forsvarsavanserte forskningsprosjektbyrås (DARPA) publikumssøkt formell verifisering (CSFV) -eksperiment lansert i 2013. Eksperimentet ble opprettet for å bekjempe de dyre, tidkrevende fallgruvene med tradisjonelle kodeverifiseringsmetoder.
Opererer på hypotesen om at "stort antall ikke-eksperter kan utføre formell verifisering raskere og mer kostnadseffektivt enn konvensjonelle prosesser", utviklet DARPA CSFV-programmet for å kontrollere store grupper av kode for nøyaktighet ved bruk av nettleserbaserte videospill.
På onsdag utlyste DARPA programmet en suksess og annonserte tillegget av fem nye spill til sin eksisterende oppstilling. Fra DARPA-bloggen:
Disse [2013] spillene oversatte aktørers handlinger i programannoteringer og assisterte formelle verifikasjonseksperter ved å generere matematiske bevis for å verifisere fraværet av viktige klasser av feil i "C" og "Java" programmeringsspråk. En innledende analyse indikerer at ikke-eksperter som spiller CSFV-spill, genererte hundretusener av merknader.
De nye titlene inkluderer puslespillere Dynamakr, Paradoks, og Binær fisjon, "science game" Ghost Map Hyperspace, og fantasy sim Monster Proof. Alle DARPAs CSFV-spill, inkludert dem fra 2013-prosjektfasen, er tilgjengelige online hos Verigames. Spillere må være 18 år eller eldre for å delta.