Crowd Sourced Formal Verification-Augmentation (CSFV-A)

Abstract : Formal verification (FV) ensures that mission-essential software is free from disruptive errors and security vulnerabilities, but requires human experts that can be quickly overwhelmed by the increasing number, size, and complexity of software systems. DARPAs Crowd Sourced Formal Verification (CSFV) program built games that recast FV problems into puzzles to make these problems more accessible, increasing the manpower to construct FV proofs. This effort supported the CSFV program by hosting the games on a public website, and analyzed the gameplay for efficiency to provide FV proofs.