Charles River Analytics presents a framework for managing, deploying, and analyzing crowdsourcing tools for formal software verification, as part of DARPA’s Crowd-Sourced Formal Verification (CSFV) program. Software should go through formal verification (FV) to ensure that mission-essential software is free from disruptive errors and security vulnerabilities. The CSFV program has been building games that break down and recast formal verification problems as discrete puzzles that are more accessible to a broad population, increasing the manpower to construct FV proofs.
