The goal of DARPA's Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) is to develop formal methods tools fully integrated into pipelined software development and maintenance processes to enable higher levels of assurance that software systems are free of defects or security vulnerabilities. These formal methods tools will be designed for software engineers in the defense and aerospace industries who are not formal methods experts. Tooling will be integrated into currently used software development pipelines, enabling a continuous flow of capabilities over time while maintaining high assurance.
Collins Aerospace, Carnegie Mellon University (CMU), Kansas State University (KSU), University of Kansas (KU), Proofcraft, UNSW Sydney, and DornerWorks have teamed to address the challenges posed by the DARPA PROVERS program, which kicked off in March 2024. Our technical plan for INSPECTA is distinguished by the following characteristics:
- Our workflow and tools will address the entire software development stack, from requirements and system models to component source code, through build and deployment on the seL4 secure microkernel, all linked by formal verification at each level.
- We will achieve scalability for complex defense systems through compositional reasoning at the system level and automated analysis of components based on powerful, cloud-based solvers.
- We will achieve the highest levels of assurance by building upon the best available technologies and leveraging our experience from recent research programs as a starting point.
- Our tools will be integrated with current defense and aerospace workflow automation processes and applied to mission critical products currently under development to demonstrate their usability, practicality, and effectiveness.
- Formal verification will be made accessible to non-formal methods experts through automated analysis with streamlined user feedback and generalized proofs that are robust to changes, allow for automated re-verification, and are augmented by automated repair tools.
- Our framework is adaptable and extendable to allow incorporation of results from other researchers, including other specification languages, other source code languages, and other operating system targets.
- Our access to critical defense and aerospace products in both commercial and military domains served by Collins will provide the basis for compelling demonstrations of INSPECTA technologies.
Tools being developed on the INSPECTA project are open-source and will be available on GitHub (stay tuned).
This video shows the US Army's Launched Effects vehicle which is planned as a demonstration platform to show the effectiveness and practicality of INSPECTA tools