In March 2024, the Defense Advanced Research Projects Agency (DARPA) awarded Stanford's Clark Barrett a Cooperative Agreement under the Research and Technology Development program. The award, titled "PEGISUS: Proof EnGineering and Integration with Satisfiability modUlo theorieS," is scheduled for completion by December 28, 2027.

The University of Iowa, Universidade Federal de Minas Gerais, and Bar-Ilan University will be subcontractors to Stanford University on the project and will conduct advanced research and development across various scientific and technological domains. While the work will be highly collaborative between university partners, each team will be responsible for specific technical tasks.

For instance, the University of Iowa team (inc. Profs. Cesare Tinelli, Garrett Morris, incoming faculty member Katherine Kosaian, as well as Associate Research Scientist Andy Reynolds, a Post Doc, and several Graduate Assistants) will work towards the following objectives:

• Develop a flexible SMT-LIB 3-based language for proof certificates and build a small and efficient proof checker for proof certificates in this language
• Instrument the cvc5 SMT solver to produce proof certificates in the SMT-LIB 3-based proof format and improve its efficiency and proof repair capability
• Integrate cvc5 into the Lean4 and Isabelle provers/proof assistants
• Instrument all tools (cvc5, Isabelle, Lean4, distributed solving framework) to provide detailed metrics and data for tasks in this proposal; measure their effectiveness.

The researchers hope that this project will encourage the use and adoption of their platform and tools by industrial collaborators (akin to AWS "calling" cvc5 SMT solver billions of times a day). They also expect that that program alumni/ae will take these ideas to the companies they work in or create.

The University of Iowa collaborators will receive $1.5 million over the next 3 years for their contribution to the project.