NL2ACSL: Interactively translating natural language to ANSI C specification language with large language models

The ANSI/ISO C Specification Language (ACSL) is widely used to describe the behavioral properties of C programs in formal verification. However, manually crafting formal program specifications requires substantial expertise and effort, which makes it time-consuming and demanding. To reduce the burden on software developers, recent advances in Large Language Models (LLMs) have inspired studies on automated specification generation. Although LLMs demonstrate strong capabilities in code understanding and generation, existing methods are limited owing to the lack of ACSL-annotated data and the need for expert intervention, making completetly automated and correct specification generation difficult. To address these challenges, this study proposes NL2ACSL, an LLM-based multi-agent framework that automatically translates natural language descriptions into formal ACSL function contracts. In NL2ACSL, the natural language description is first analyzed to identify the intended functional requirements. These requirements are then aligned with an ACSL knowledge base using retrieval-augmented generation (RAG), which provides grammar patterns and logic templates for specification construction. The retrieved context is passed to a specification generation agent that uses chain-of-thought (CoT) prompting to generate candidate ACSL annotations. Finally, a dedicated evaluation agent trained using reinforcement learning selects the specification that best preserves semantic intent while adhering to ACSL syntactic rules. Experimental results show that NL2ACSL achieves verification success rates of 74.4% and 69.5% with GPT-4o and DeepSeek-V3, respectively, outperforming existing LLM-based methods and demonstrating improved accuracy and applicability in formal software verification.