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

1 Introduction

• Eiffel is low-resource, and its limited public code makes LLM code generation more challenging despite first-class specifications and the AutoProof static verifier.Adapter tools should structure and contextualize code for the model while presenting reasonable outputs to the user.Source: §1 · p. 2
• Eiffel-tools implements the Language Server Protocol to integrate an adapter conveniently into most code editors.It directs the LLM with relevant code and connects the interaction loop to a verifier.Source: §1 · p. 2
• The highlighted fix-feature-body command is evaluated on two datasets of buggy programs with correct specifications using three LLMs.The models include a small generalist, a small coding model, and a larger coding model.Source: §1 · p. 2

2.1 Eiffel and AutoProof

• Eiffel embeds preconditions, postconditions, and class invariants in source code, while AutoProof proves functional correctness for model-based contracts across possible execution paths.Unlike runtime contract checks, static verification can prove properties without executing the program.Source: §2.1 · pp. 2–3

2.2 Large language models for software development

• LLMs need explicit context because coherent outputs do not make them oracles that can infer unstated user intentions.The paper expects language- and project-specific context to partially compensate for scarce training data in low-resource languages.Source: §2.2 · p. 3

2.3 Language server protocol

• LSP offers a common integration point between editors, verifiers, and LLMs, while standardizing editor features such as code actions and commands.LSP custom operations can access server state and project-specific knowledge to guide generation and support verification of generated code against specifications.Source: §2.3 · pp. 3–4

3 Related work

• Several reviews survey LLM applications and challenges across software engineering, including generative transformations and development processes.The cited reviews cover requirements, testing, deployment, and operations.Source: §3 · p. 4
• Prior work uses language-server completion engines to provide context during LLM inference, whereas this work defines where and how project-specific knowledge enters prompts.The cited monitor approach dynamically masks streaming model output.Source: §3 · p. 4
• CITADEL and AutoInfer generate Eiffel contracts for dynamic checks, while AutoFix and Proof2Fix repair Eiffel programs using testing or AutoProof.The paper distinguishes its focus on LLM-guided, project- and language-specific specification and verification workflows.Source: §3 · pp. 4–5
• Other related studies examine specification generation and repair and developers producing verified fixes with or without LLM chat assistance [22].Source: §3 · p. 5

4 Design and implementation

• Eiffel-tools provides LLM-powered commands for generating or repairing Eiffel code and specifications, using a static verifier.It indexes project information and incorporates relevant context into prompts without relying on a full Eiffel compiler.Source: §4 · p. 5

4.1 Interactive commands

• Interactive commands are IDE code actions that can add model-based contracts to preconditions and postconditions, filtering unsuitable suggestions before insertion.The tool removes redundant or unusable contracts, including those with invalid identifiers or incorrect call arguments.Source: Add model-based contracts · p. 6
• The interactive fix-feature-body command changes only a feature body and uses an LLM–AutoProof loop to seek a body satisfying its specifications.The command leaves specifications unchanged.Source: Fix feature body · p. 6

4.2 Non-interactive commands

• Non-interactive feature-by-feature correction prompts the LLM with code and verification or compilation errors, while treating contracts as correct and unmodifiable.Each candidate is tested with AutoProof; failed candidates are reverted and another is tried up to a limit.Source: Feature by feature body correction · p. 9
• Class-by-class correction verifies and repairs a whole class, potentially changing both specifications and code in one candidate output.The command backs up the class and retries after reverting candidates that fail verification.Source: Class by class correction · p. 9

5 Evaluation

• Each bug receives up to 10 repair attempts, with verification errors fed back to the model and each unverified candidate carried into the next attempt.The evaluation covers the feature-by-feature body correction command.Source: §5 · p. 11

5.1 Models

• The experiment compares Claude Sonnet 4.6, the “expensive but powerful” coding and complex-agent option, GPT-5 Nano, the “cheap but fast” lower-latency, lower-cost option, and free, open-weight Poolside Laguna XS [27].Source: §5.1 · p. 11

5.2 Datasets

• The benchmark uses 513 buggy-java-jml-eiffel examples translated from BuggyJava+JML and all 26 maple-recursive-eiffel examples translated from Maple.Both datasets contain buggy programs with formal contracts; their examples include algorithms, data structures, and recursive functions.Source: §5.2 · pp. 11, 13

5.3 Ablations

• The two prompt ablations contrast a full prompt with Eiffel syntax guidance, a feature template, available-variable information, and verification errors against a minimal prompt omitting most rich features.The full-prompt feature template is shown in Fig. 5.Source: §5.3 · pp. 13–14, Figure 5 · p. 13
• The full prompt requires a single Eiffel code block that preserves the feature header and contracts while supplying corrected local declarations and body.The required structure ends with the postcondition and closing end.Source: §5.3 · p. 13

6 Results and Discussion

• 95% of bugs were fixed by Sonnet 4.6 with full prompts, versus 90% with minimal prompts; Laguna and GPT-5 Nano switched order across ablations.With full prompts, Laguna fixed 85% versus GPT-5 Nano’s 82%; with minimal prompts, GPT-5 Nano fixed 77% versus Laguna’s 76%.Source: §6 · p. 14, Figure 6 · p. 14
• 6.4 pp average improvement came from full prompts; Laguna gained the most, improving by 8.9 pp.The reported prompt effect averaged across models; Laguna’s gain was the largest.Source: §6 · p. 14
• Most fixes occurred on the first attempt, from 67.9% for Laguna with minimal prompts to 83.5% for Sonnet with minimal prompts; later attempts added progressively less success.Full prompts produced a higher success rate consistently from the second attempt onward.Source: §6 · p. 15, Figure 7 · p. 15
• With minimal prompts, total time per feature increased, mainly alongside the greater number of attempts; smaller models spent most time waiting for the LLM.For Sonnet, LLM time was similar to verification and tool time.Source: §6 · p. 15, Figure 8 · p. 16
• Sonnet’s usage per feature cost 5x GPT’s with full prompts and 3.3x with minimal prompts, but Sonnet was 2x and 3.3x faster, respectively.Minimal prompts decreased Sonnet’s cost per feature but increased GPT’s; the paper attributes this difference to more attempts and reasoning tokens.Source: §6 · pp. 15, 17, Figure 9 · p. 16, Figure 10 · p. 17

• Public benchmarks may have leaked into some models’ training data, allowing them to reproduce trained solutions rather than fix bugs.Source: §7 · p. 17

8 Conclusion and Future work

• Eiffel-tools uses an LSP server as both the LLM harness and the integration interface between the editor, verifier, and LLM.The implementation includes advanced code-editing actions combining LLMs and formal verification.Source: §8 · p. 17
• The experiment establishes a baseline for improvements across fix success rate, time, and cost, while discussing trade-offs among these axes.Source: §8 · p. 18
• Further prompt-ablation analysis is needed to identify an optimal initial prompt and assess possible tool-call and MCP interfaces for the compiler and verifier.Source: §8 · p. 18
• The authors plan to extend Eiffel-tools and analyze the performance of new code actions.Source: §8 · p. 18