An Eiffel Language Server Wiring LLMs to a Static Verifier Fixes 76-95% of Bugs

arXiv 2609.03086·medium signalXBlueskyLinkedInCopy link

arXiv 2609.03086 presents Eiffel-tools, an LSP implementation that uses LLMs to produce code and specifications for statically verified software, crafting rich programmatic prompts from language- and project-specific knowledge, verifying output with a static verifier, and correcting or rejecting it while handling retries until the program passes verification. Evaluated on two public datasets with three models, it fixes 76% to 95% of bugs depending on model and prompt, with the results exposing a trade-off between number of fixing attempts and success rate. The architectural point for builders is that the LSP already holds the project-specific context an agent needs, so the language server is a natural place to put the generate-verify loop.