Large Language Models and Language Server Protocol: a match made in context

Specification-driven development (SDD) is getting more attention with the growing use of Large Language Models (LLMs) for development [1]. In this approach, the development is done in a natural language by writing specifications while the program code is then generated automatically from the specifications.

Expressing specifications using a formal language, even partially [2], opens the door for various analysis tools. For example, using Design by Contract [3] in Eiffel, the program’s state is checked against specifications during execution. This allows test runs of the program to show the presence of implementation errors.

A more advanced analysis such as formal verification allows finding inconsistencies between specifications and implementation statically, without running the code. This allows finding errors earlier and mathematically proving arbitrary functional properties. Still, errors in specifications can lead to invalid but correct programs.

Modern SDD relies heavily on LLMs. While LLMs code generation might work well for programming languages that are well-represented in the training datasets, their ecosystem might not have formal verification tools available. These are called high-resource languages [4].

Eiffel is a low-resource language; it has a first-class support for specifications and a static verifier AutoProof, but the low amount of public code makes LLM code generation more challenging. Adapter tools could mitigate this issue. Any such tool must structure and contextualize the code for the model and must keep the user in the loop whenever a reasonable output is produced. To mitigate this issue, special tools can be implemented which take the role of an adapter: on the one hand, the tool must structure and contextualize the code for the model, on the other hand, the tool must present model’s outputs to allow the user to benefit more from the LLM.

This paper introduces Eiffel-tools [5], as the aforementioned adapter. Eiffel-tools implements the Language Server Protocol (LSP) to integrate conveniently in the majority of code editors.

In this paper we highlight the tool’s “fix feature body” command. The command tries to change the body of the procedure such that it will satisfy its specifications. The tool presents the relevant parts of the code, while omitting irrelevant parts of the project, to the LLM and sets up the interaction loop between the LLM and the verifier.

We present the evaluation of this command using two datasets of buggy programs with correct specifications and compare the performance of three LLMs. One model is a small generalist model, second is a small coding model and another is a bigger coding model.

The remainder of this paper is structured as follows. Section 2 provides the necessary background, introducing the core concepts related to the Eiffel programming language, large language models, and LSP-based tooling in greater detail. Section 3 reviews related work in automated program repair, LLM-assisted development, and contract-driven methodologies. Section 4 presents the design and implementation of our experimental setup, describing how contract-guided repair is operationalized using LLMs. Section 5 outlines the evaluation methodology, followed by Section 6, which reports the experiment results and discusses them. Section 7 addresses threats to validity and limitations of the study. Finally, Section 8 outlines directions for future work.

This section provides the background information about the Eiffel programming language and the related technologies.

The research area applying LLMs to software engineering is flourishing, with a rapidly expanding body of work addressing a wide range of development and analysis tasks. Authors of [10] provide a systematic taxonomy of generative transformations and their compositional patterns in LLM-native applications, primarily as an analytical framework. Another study [11] conducts a systematic literature review of LLM applications in SE, with a particular focus on understanding how LLMs can be exploited to optimize processes and outcomes. Complementary to these studies, the authors [12] systematically review recent advances in LLM applications for software engineering. They analyze applications in requirements, testing, deployment, and operations, and identify key challenges and future directions.

The study [13] emphasizes on the investigation of the emerging area of LLMs for SE and their applications, highlighting the importance of hybrid techniques, such as traditional SE plus LLMs for the reliable and efficient software development.

LSP can be used to provide context during the LLM inference through monitors [14]. This approach uses language servers externally, primarily leveraging their completion engines, to dynamically mask the streaming output of large language models, which further enhances fine-tuning and dynamic masking. With the same philosophy, our work defines where and how the LLMs may find language and project specific knowledge, which adds benefit to fine-tuning and dynamic masking.

CITADEL [15] and AutoInfer [16] automatically generate Eiffel specifications. Citadel is an Eiffel front end for Daikon [17]. AutoInfer [16] is another tool that generates Eiffel contracts using data mining and contract templates. However, these tools generate specifications for dynamic checks, not model-based specifications for static verification.

On the side of automatic repair of Eiffel programs there is AutoFix [18] and Proof2Fix [19]. AutoFix uses random testing through AutoTest [20] to identify the faults. Proof2Fix identifies faults using AutoProof. They both propose candidate fixes that may be the substitution of a template for code edits or the strengthening of the preconditions or weakening of the postconditions for contracts edits. However, these tools are limited to Eiffel and do not generalize to LLM-guided, project- and language-specific specification and verification workflows, which is the focus of our approach.

An experiment similar to the evaluation of this paper is presented in [21] with the focus on generating specifications and fixing them. Similar prompting techniques are discussed for JML and Frama-C.

A close work in the field of LLM-assisted development and manual program repair is the study [22] of developers producing verified fixes with and without the assistance of an LLM chat.

Eiffel-tools is an LSP language server which provides several novel commands using LLMs and a static verifier to generate or repair Eiffel code and specifications.

The language server avoids using a full-fledged Eiffel compiler to be performant and provide support to projects in inconsistent states with compilation errors and missing files. Eiffel-tools reads the project configuration file (ECF), parses it, extracts the used libraries and recursively analyses them. All classes used in the system are indexed (features, contracts, inheritance tree is stored) and available through the usual LSP interfaces which allows code editors, for example, to display and navigate between classes and features in the source code. This information is also integrated into LLM prompts when relevant to give the relevant context to the model.

Eiffel source code in files and LLM responses is parsed using an external parser [23] based on Tree-sitter [24]. This allows using Tree-sitter queries to extract the relevant structures from the source code. For example, when LLM is used to generate code, the parser is used to find valid features in the responses and then to extract code or contracts of the found feature.

The tool does not depend heavily on any specific LLM or an API. Currently an OpenAI-like chat/completions API is supported. We are using the OpenRouter platform which provides access to several LLMs using the same API to conduct the experiment.

Eiffel-tools uses AutoProof to verify existing code or LLM-generated suggestions. Because AutoProof may not terminate on some inputs, Eiffel-tools runs it with timeouts: any verification exceeding a time limit is killed, and if the code was LLM-generated, the tool reverts it to its previous stable state upon failure.

For organizational clarity, Eiffel-tools commands are classified along two dimensions:

• •

  By interaction mode

  • –

    Interactive, invoked as code actions by the LSP client

  • –

    Non-interactive, invoked as standalone executables

• •

  By focus

  • –

    specifications

  • –

    code

  • –

    specification and code

We evaluated the feature by feature body correction command, described in Section 4.2, on the datasets buggy-java-jml-eiffel and maple-recursive-eiffel using three LLMs, GPT-5 Nano, Claude Sonnet 4.6 and Poolside Laguna XS with 2 ablations (versions) of prompts used.

For every bug fixing task, 10 attempts were made by Eiffel-tools to fix the error. Each attempt included the initial verification, prompting the model with the verification result, verifying the suggested fix. If the suggested fix does not verify, it is kept and the next attempt starts with the previously suggeste fix, enabling a feedback loop between LLM and the verifier.

All evaluations are in Eiffel-tools repository within the corresponding folder experiment-results [5].

In total, the experiment used 539 bugs to be fixed by 3 LLMs using 2 prompt ablations. At most 10 attempts were allowed per feature.

Figure 6 shows how many bugs were fixed by each model in every ablation.

Sonnet 4.6 solved the most tasks in both ablations (95% full, 90% minimal). Laguna XS was better than GPT-5 nano in “full” (85% vs. 82%) while GPT was better than Lagune in “minimal” (77% GPT vs. 76% Laguna).

Using “full” gives 6.4 pp improvement on average. Extended prompts helped Laguna to improve the most (8.9 pp).

Figure 7 shows the cumulative success rate per the number of attempts used. The majority of fixes happen on the first attempt (from 67.9% for Laguna “minimal” to 83.5% for Sonnet “minimal”). Every next attempt increases the success rate less and less.

The “full” ablation results in a higher success rate consistently starting from the 2nd attempt.

Figure 8 shows the mean time used per feature run, including both sucessfully fixed and still unfixed features after all attempts are exhausted. The diagram shows the time spent in the LLM (waiting for the model response) separately from the time spent in other steps (verification, tool overhead).

LLM time depends on the model itself and the provider’s API. While there are several configurable settings in OpenRouter which can optimize throughput and latency, the experiment used the default settings.

Experiments using smaller models spent the majority of time waiting for LLM while Sonnet’s LLM time was similar to verification + tool time.

Using the “minimal” ablation increases the total time per feature which is mainly connected with the increase in the number of attempts used.

Figure 9 present the mean cost used per feature run, including both sucessfully fixed and unfixed features.

Because Laguna was available for free at the time of writing and no pricing information was known, only Sonnet 4.6 and GPT-5 nano are compared.

While Sonnet’s usage per feature is more expensive than of GPT (5x in “full” and 3.3x in “minimal”), Sonnet is faster (2x in “full”, 3.3x in “minimal”).

Switching to the “minimal” ablation decreased the cost per feature when using Sonnet but increased when using GPT. The difference can be attributed to the increase in attempts needed and the increase in reasoning tokens (Figure 10).

In the experiment Sonnet had reasoning disabled (default settings) but GPT and Laguna have reasoning enabled. Reasoning tokens have the same cost as output tokens and cost more (5x more expensive for Sonnet, 8x more expensive for GPT). Minimal ablation triggers additional reasoning in GPT which increases the cost.

The benchmarks used in our evaluation, described in Section 5, are public and available in multiple programming languages, either C and Eiffel or Java-JML and Eiffel. It is possible that those benchmarks leaked in the training data of some LLMs and the models could reproduce the solution they were trained on instead of “fixing” the bug.

This paper presented an approach for using an LSP server as both the LLM harness and the integration interface between the editor, verifier and LLM at the same time. Implementation of several advanced code editing actions combining LLMs and vormal verification is presented.

The experiment results discuss trade-offs and set a baseline for the possible further improvements across several axes: fix success rate, time, and cost.

Further analysis of prompt ablations is needed to identify optimal initial prompt and the possible extension of the system with “tool calls” and presenting an MCP (Model Context Protocol) interfaces for the compilar and verifier.

Authors plan extending the implementation of Eiffel-tools and analysing performance of new code actions.