Declarative specification languages like Alloy are critical for modeling and verifying complex software systems, yet repairing these specifications remains a significant challenge for ensuring software dependability. This study conducts the first comprehensive empirical evaluation comparing traditional systematic repair techniques with emerging Large Language Model (LLM)-based approaches across two established benchmarks, analyzing over 1,900 Alloy specifications. By systematically analyzing repair success rates, ground truth similarity, and repair generation strategies, we reveal nuanced performance characteristics of different repair methodologies. Our findings demonstrate that while traditional tools excel in systematic fault localization and achieving high ground truth similarity, LLM-based techniques—particularly multi-round prompting approaches—offer unique capabilities in addressing complex specification errors, with some hybrid approaches achieving repair rates of up to 85.5%. Critically, we show that integrating traditional fault localization techniques with LLM-based repair strategies can significantly enhance overall repair effectiveness and specification dependability. This research provides a large-scale empirical evaluation of how various Alloy repair techniques work in synergy, offering valuable insights that chart a promising path for future automated specification repair approaches and contribute to the development of more reliable and secure software systems.

Abstract Automatic Program Repair (APR) has garnered significant attention as a practical research domain focused on automatically fixing bugs in programs. While existing APR techniques primarily target imperative programming languages like C and Java, there is a growing need for effective solutions applicable to declarative software specification languages. This paper systematically investigates the capacity of Large Language Models (LLMs) to repair declarative specifications in Alloy, a declarative formal language used for software specification. We designed six different repair settings, encompassing single-agent and dual-agent paradigms, utilizing various LLMs. These configurations also incorporate different levels of feedback, including an auto-prompting mechanism for generating prompts autonomously using LLMs. Our study reveals that dual-agent with auto-prompting setup outperforms the other settings, albeit with a marginal increase in the number of iterations and token usage. This dual-agent setup demonstrated superior effectiveness compared to state-of-the-art Alloy APR techniques when evaluated on a comprehensive set of benchmarks. This work is the first to empirically evaluate LLM capabilities to repair declarative specifications, while taking into account recent trending LLM concepts such as LLM-based agents, feedback, auto-prompting, and tools, thus paving the way for future agent-based techniques in software engineering.