Building systems in proof assistants is challenging for many reasons. Such systems must tolerate changes gracefully: definitions may be optimized for performance, new theorems may be added, and the proof assistant itself may change how tactics work. Proof assistants are also highly expressive; engineers must ensure that their specifications do not accidentally allow for undesirable behavior. Furthermore, large-scale developments often depend on good tactic performance, requiring developers to reason about low-level performance costs.

To help address these challenges, the Proof Engineering (PE) project is collecting best practices and building techniques and tools for developing large systems in the demanding and foundational context of proof assistants.

May 2019 Paper in ITP 2019.

Nov 2018 Won a research award from Facebook.May 2018 Paper in ISSTA 2018.

Feb 2018 Paper in ICSE-Demo 2018.

Nov 2017 Papers in ASE 2017 and CPP 2018.

May 2017 Site goes live.

- Talia Ringer, Nathaniel Yazdani, John Leo and Dan Grossman. Ornaments for Proof Reuse in Coq. To appear in Proceedings of Interactive Theorem Proving (ITP), 2019.
- Karl Palmskog, Ahmet Celik, and Milos Gligoric. piCoq: Parallel Regression Proving for Large-Scale Verification Projects. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), 2018.
- Ahmet Celik, Karl Palmskog, and Milos Gligoric. A Regression Proof Selection Tool For Coq. In Proceedings of the International Conference on Software Engineering (ICSE), Demo Papers, 2018.
- Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Adapting Proof Automation to Adapt Proofs. In Proceedings of the ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), 2018.
- Ahmet Celik, Karl Palmskog, and Milos Gligoric. iCoq: Regression proof selection for large-scale verification projects. In Proceedings of 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), Urbana, IL, USA, 2017, pp. 171-182.

- Regression proof selection (iCoq and Chip)
- Proof repair (PUMPKIN-PATCH)
- Proof engineering bibliography (proofengineering-bib)
- Survey of proof engineering theory, techniques, tools, and best practices
- Ornamental search (DEVOID)

Proof Engineering is an international collaboration between researchers at University of Washington (UW), Yale-NUS College (Yale-NUS), The University of Texas at Austin (UT), and Cornell University (CU). Many volunteers have helped out on PE projects; we're very grateful for their contributions! Folks currently working on PE include:

- Ahmet Celik (UT)
- Ryan Doenges (CU)
- Milos Gligoric (UT)
- Dan Grossman (UW)
- Karl Palmskog (UT)
- Talia Ringer (UW)
- Ilya Sergey (Yale-NUS)
- Zach Tatlock (UW)
- James Wilcox (UW)
- Doug Woos (UW)