PEARLS: Proof Engineering, Adaptation, Repair, and Learning for Software

Given the successful deployments of proof tools in the Department of Defense (DOD) and industrial practice, there is growing interest in adopting formal proofs to provide assurance for software. 

Such tools provide a level of assurance not possible through testing alone. However, analysis has been hampered by the limited size and complexity of problems that can be addressed, and the highly specialized skills needed to exercise formal verification tools. As a result, the ability to objectively determine that software contains no flaws, with respect to a specification, is very limited. 

Moreover, any attempt to update or maintain the software can invalidate a formal proof, requiring significant effort to repair the proofs.

The Proof Engineering, Adaptation, Repair, and Learning for Software (PEARLS) AI Exploration topic seeks novel methods of developing formal proofs that can be trained on limited data to significantly improve formal proof construction, evolution, or repair. 

As scalable proof repair techniques are developed, proofs would be integrated into the normal software development process with the need for formal methods expertise being limited to the most difficult cases. 

Then existing proof technologies could be applied in many more software engineering contexts in support of critical DOD national security systems using a comparable effort of maintaining a proof to that of maintaining the software. Moderate code changes would result in moderate – and automated – proof repairs.