Początkowa faza eksperymentalnej formalnej weryfikacji (CSFV) przeprowadzonej przez US Army's Defense Advanced Research Projects (DARPA) w 2013 r. Eksperyment został stworzony w celu zwalczania kosztownych, czasochłonnych pułapek tradycyjnych metod weryfikacji kodu.
Działając zgodnie z hipotezą, że „duża liczba nie-ekspertów może przeprowadzić formalną weryfikację szybciej i bardziej efektywnie niż konwencjonalne procesy”, DARPA zaprojektowała program CSFV, aby sprawdzać duże partie kodu pod kątem dokładności przy użyciu gier wideo opartych na przeglądarce.
W środę DARPA ogłosił sukces programu i ogłosił dodanie pięciu nowych gier do istniejącego składu. Z bloga DARPA:
Te gry [2013] przetłumaczyły działania graczy na adnotacje programowe i pomogły ekspertom ds. Weryfikacji formalnej w wygenerowaniu dowodów matematycznych w celu zweryfikowania braku ważnych klas wad w językach programowania „C” i „Java”. Wstępna analiza wskazuje, że nie-eksperci grający w gry CSFV wygenerowali setki tysięcy adnotacji.
Nowe tytuły zawierają układanki Dynamakr, Paradoks, i Binarne rozczepienie, „gra naukowa” Hiperprzestrzeń Mapa duchówi sim fantasy Dowód potwora. Wszystkie gry CSFV DARPA, w tym te z fazy projektu 2013, są dostępne online w Verigames. Gracze muszą mieć ukończone 18 lat, aby wziąć udział.