发表机构
Constructor Institute of Technology; Constructor University（Constructor理工学院; Constructor大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文介绍了结合LLM与形式验证器的Eiffel-tools工具，用于辅助Eiffel语言的静态验证软件开发，其漏洞修复率达76%-95%，且修复次数与成功率存在权衡。
AI 中文摘要
本文介绍了Eiffel-tools，这是一款针对Eiffel编程语言的语言服务器协议（LSP）实现，它利用大语言模型（LLM）辅助开发经静态验证的软件。该工具提供多种交互式和非交互式命令以生成代码和规格说明，它运用语言及项目特定知识精准引导LLM，并通过静态验证器对输出进行验证。它为输入精心设计了丰富的程序化提示，同时修正或拒绝输出，还会进行重试直至程序通过验证。该工具的漏洞修复能力在2个公开数据集上使用3种模型进行评估，结合LLM和形式验证器，该工具可修复76%至95%的漏洞，具体比例取决于所用模型和提示。结果显示修复尝试次数与成功率之间存在权衡关系。
英文摘要
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.
CommentsSubmitted and presented at VERIFAI-2026
