Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS)
Abstract
The Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) program is creating the science and technology needed for continuous reasoning about complex systems that can support software development pipelines. These mathematically based techniques, or formal methods, enable rigorous modeling, reasoning, and proving diverse properties of software code or design models, for example, the absence of a specific type of defect or security vulnerability. PROVERS integrates formal methods into a modern incremental and iterative development process by running tools at each code commit and delivering results to developers when they can most effectively remediate discovered issues. To achieve this, PROVERS is focusing on creating and sustaining a body of evidence that can co-evolve with the system under change to support continuous assessment and ensure that the system remains free of identified categories of defects and security vulnerabilities through its lifetime. Key PROVERS objectives include enabling proof maintenance and repair capabilities at a cost that is proportionate to code change; integration of formal methods with code, properties, and proofs in a single workflow that reduces human involvement; providing improved explanations to facilitate proof repair; and automating formal methods-based software analysis to support software developers that are not formal methods experts. PROVERS science and technology will facilitate the agile development and continuous improvement of mission-critical software systems that meet the high security and quality standards required by the DoD. Beginning in FY 2025, this program is funded in PE 0602303E, Project IT-03.
Document Details
- Document Type
- Accomplishment
- Publication Date
- Oct 01, 2025
- Source ID
- 7ac507d8ea6431a8ef22cac8d17f55c8