अमेरिकी सेना की डिफेंस एडवांस्ड रिसर्च प्रोजेक्ट्स एजेंसी (DARPA) के शुरुआती चरण में भीड़-खट्टा औपचारिक सत्यापन (CSFV) प्रयोग 2013 में शुरू किया गया था। यह प्रयोग पारंपरिक कोड सत्यापन विधियों के महंगे, समय लेने वाले नुकसान से निपटने के लिए बनाया गया था।
DARPA ने ब्राउज़र-आधारित वीडियो गेम का उपयोग करके सटीकता के लिए बड़े बैचों की जांच करने के लिए CSFV कार्यक्रम को डिज़ाइन किया, "परिकल्पना पर काम करते हुए कि" बड़ी संख्या में गैर-विशेषज्ञ पारंपरिक प्रक्रियाओं की तुलना में औपचारिक सत्यापन तेजी से और अधिक लागत-प्रभावी ढंग से कर सकते हैं।
बुधवार को, DARPA ने कार्यक्रम को सफल घोषित किया और अपने मौजूदा लाइनअप में पांच नए खेलों को शामिल करने की घोषणा की। DARPA ब्लॉग से:
इन [2013] गेम्स ने खिलाड़ियों के कार्यों को प्रोग्राम एनोटेशन में अनुवादित किया और "C" और "Java" प्रोग्रामिंग भाषाओं में दोषों के महत्वपूर्ण वर्गों की अनुपस्थिति को सत्यापित करने के लिए गणितीय प्रमाण बनाने में औपचारिक सत्यापन विशेषज्ञों की सहायता की। एक प्रारंभिक विश्लेषण बताता है कि CSFV गेम खेलने वाले गैर-विशेषज्ञ ने सैकड़ों हजारों एनोटेशन उत्पन्न किए।
नए शीर्षकों में गूढ़ व्यक्ति शामिल हैं Dynamakr, विरोधाभास, तथा बाइनरी विखंडन, "विज्ञान खेल" भूत का नक्शा हाइपरस्पेस, और फंतासी सिम राक्षस प्रमाण। DARPA के सभी CSFV गेम, जिनमें 2013 प्रोजेक्ट चरण के लोग शामिल हैं, वेरीगैम पर ऑनलाइन उपलब्ध हैं। गेम खेलने वालों की उम्र 18 वर्ष या उससे अधिक होनी चाहिए।