Formal verification is typically a tedious and costly affair performed by highly-trained and highly-paid engineers. We would like to change that, making it as fun as a game and accessible to people without any knowledge of computer science. We would like people to prove properties of programs while they wait for the bus, by playing a game on their phones.
To that end, we are creating a system, which we call Verification Games, to crowd-source program verification. Our system takes as input a program, and produces as output a game. When a person finishes a level of the game, then the final configuration of board elements can be translated into a proof of a property about the program. Then, the player can move on to a different level, which corresponds to a different property about the program, or a property about a different program.
Danger Room blog recently mentioned this work (see the end of the article). The DARPA slide has a screenshot of our game Pipe Jam. DARPA has announced a new Crowd-Sourced Formal Verification program that is inspired by our work.