PROVERS: Pipelined Reasoning of Verifiers Enabling Robust Systems

Engineering practices for software-reliant systems have evolved steadily over many decades, and so too have the assurance techniques that confirm systems’ correctness and security.

Through a nascent discipline known as proof engineering, DARPA seeks to create higher levels of assurance that will help critical DOD software systems remain free of certain classes of defects and vulnerabilities.

Proof engineering will help developers construct software safely and ensure the software meets specified assurance requirements. DARPA’s Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) program will develop formal methods tools to guide software engineers through designing proof-friendly software systems and reduce the proof repair workload.

PROVERS builds off the Proof Engineering, Adaptation, Repair, and Learning for Software (PEARLS) AI Exploration project, which demonstrated how AI and machine learning could support and automate the generation and maintenance of proofs used in the formal verification of software at large scale.

The goal of PROVERS is to make formal methods accessible to non-experts (e.g., traditional software developers and systems engineers) while minimizing the impact on their existing processes and performance. Furthermore, the tooling would integrate into a development pipeline enabling a continuous flow of capabilities over time while maintaining high levels of assurance.

PROVERS is a 42-month program spanning three phases that encompasses proof engineering, platform development, a red team to emulate potential adversaries’ attacks, and a separate federally funded research and development center to provide quantitative evaluation and evidence curation.