Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper presents Eiffel-tools, an innovative language server protocol (LSP) for the Eiffel programming language that leverages Large Language Models (LLMs) to enhance the development of statically verified software. By integrating language-specific knowledge and a static verifier, Eiffel-tools generates tailored prompts for code generation and correction, achieving a bug-fixing success rate of 76% to 95% across different models and datasets. The findings highlight a critical trade-off between the number of fixing attempts and the overall success rate, underscoring the potential of combining LLMs with formal verification methods in software development.
Eiffel-tools can fix up to 95% of bugs in statically verified software by intelligently combining LLMs with formal verification.
This article introduces Eiffel-tools, a language server protocol (LSP) implementation for the Eiffel programming language that uses Large Language Models (LLMs) to aid the development of statically verified software. The tool provides various interactive and non-interactive commands to produce code and specifications. It uses language and project specific knowledge to precisely direct the LLM and verifies the output using a static verifier. It crafts rich programmatic prompts for the input and corrects or rejects the output. Furthermore, it handles the retries until the program passes verification. The tool's bug fixing capability is evaluated on 2 public datasets using 3 models. The tool can fix 76% to 95% of bugs by combining LLMs and a formal verifier depending on the model and prompts used. The results show the trade-off between the number of fixing attempts and the success rate.