Proof engineering in Coq is a labor-intensive process, and as proof developments grow in size, redundancy and maintainability become significant challenges. One such redundancy is \textit{goal cloning}, i.e., proving $\alpha$-equivalent goals multiple times, leading to wasted effort and bloated proof scripts. In this paper, we introduce clone-finder, a novel technique for detecting goal clones in Coq proofs. By leveraging the formal notion of $\alpha$-equivalence for Gallina terms, clone-finder systematically identifies duplicated proof goals across large Coq codebases. We evaluate clone-finder on 40 real-world Coq projects from the CoqGym dataset. Our results reveal that each project contains an average of 16.9 instances of goal clone. We observed that the clones can be categorized as either \textit{exact goal duplication}, \textit{generalization}, or \textit{$\alpha$-equivalent goals with different proofs}, each signifying varying levels duplicate effort. Our findings highlight significant untapped potential for proof reuse in Coq-based formal verification projects, paving the way for future improvements in automated proof engineering.

Ali Ghanbari is currently an assistant professor in the Department of Computer Science and Software Engineering at Auburn University. Ghanbari received his Ph.D. in Software Engineering from The University of Texas at Dallas. Previously, he earned his Master’s and Bachelor’s degrees in Software Engineering from Amirkabir University of Technology (Tehran Polytechnic). From 2022 to 2023, he worked as a Postdoctoral Research Associate at Iowa State University under CIFellows 2021 program.

Ghanbari’s research spans the intersection of programming languages, software engineering, and machine learning. He employs programming languages and machine learning techniques to address core challenges in software engineering, such as testing, verification, and automated repair. And he also leverages programming languages and software engineering methods to simplify the construction, reliability, and quality assurance of machine learning-based systems.

He is the recipient of multiple NSF awards and the ACM SIGSOFT Distinguished Paper Award at the 38th IEEE/ACM International Conference on Automated Software Engineering (ASE 2023).