Агентство по перспективным оборонным научно-исследовательским разработкам США (DARPA) проводит эксперименты с созданием online-игр, позволяющих привлечь обычных пользователей для верификации надёжности и безопасности открытого ПО. Экспертов для проведения аудита качества кода не хватает, поэтому DARPA рассматривает варианты привлечения к проверке кода обычных пользователей, косвенно используя игровой процесс для организации верификации.
В настоящее время уже подготовлено пять игр (CircuitBot, Flow Jam, Ghost Map, StormBound, Xylem), которые мало отличаются по игровому процессу от типичных логических игр и головоломок. Как правило, задачей игрока является поиск оптимального пути, разбор запутанных комбинаций и организация взаимодействия между игровыми объектами. При этом, проходя множество игровых уровней пользователи невольно участвуют в процессе формальной верификации, подтверждающей надёжность работы тех или иных участков кода, взаимодействие с которыми вовлечено в игровую логику.
Игровые приложения, в которых изначально отражены математические модели исследуемых приложений, транслируют действия пользователя в программные аннотации и генерируют математические доказательства, позволяющие убедиться в отсутствии различных классов дефектов в коде на языках Си и Java. Программа формальной верификации (CSFV, Crowd Sourced Formal Verification) нацелена на подтверждение безопасности серии открытых проектов, используемых в военных и государственных учреждениях, а также в критичных к надёжности областях коммерческого сектора.
Проходящие верификацию открытые проекты не называются явно, но в опубликованном несколько лет назад документе о проведении конкурса на разработку технологии формальной верификации упоминались ядро Linux, BIND и Hadoop. Заявлено, что все выявляемые в процессе верификации ошибки оперативно сообщаются основным разработчикам проектов.
