The U.S. Defense Advanced Research Projects Agency (DARPA) has awarded BAE Systems’ FAST Labs research and development organization a $6 million contract as part of the Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) program.
Current formal methods tools, a type of software verification, provide high levels of assurance through mathematical proofs that certain properties hold, but can be time-consuming and difficult to learn and use. These proofs also need to be re-written at every code or specification change, which fails to 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.
Under the terms of the contract, BAE Systems will provide a Department of Defense (DoD)-relevant system to demonstrate how formal methods tools can integrate into the development and certification process and provide assurance of correctness. The company’s software engineers will also provide feedback to developers on how to ensure formal methods tools are applicable to DoD systems and how to make those tools accessible to them.
Work on this program will take place at BAE Systems’ facilities in Merrimack, New Hampshire; Burlington, Massachusetts; and Arlington, Virginia.
