CSFV (Crowd Sourced Formal Verification)

Formal verification is the most rigorous way to thwart attacks against IT systems and applications upon which military, government, and commercial organizations rely. Traditional formal methods, however, require specially trained engineers to manually scour software—a process that up to now has been too slow and costly to apply beyond small software components.

In contrast, CSFV games such as StormBound translate players’ actions into program annotations and generate mathematical proofs to help verify the absence of important classes of flaws in software written in the C programming language. We have developed an automated process that creates new puzzles for each verification problem in need of a solution.

With StormBound, we aim to investigate whether large numbers of non-experts playing the game can perform formal verification faster and more cost-effectively than conventional processes.