Vera needs a Language Server Protocol (LSP) implementation to enable integration with coding agents and IDEs.

Motivation

Every production coding agent (Claude Code, Cursor, Copilot, OpenHands) relies on LSP for structured code intelligence. The ETH Zurich typed-holes paper (OOPSLA 2024) showed that integrating type context from a language server into LLM prompts significantly improves completion quality. Without LSP, agents fall back to grep-based navigation and lose access to Vera's rich type information.

Proposed features

• Diagnostics — publish structured errors/warnings on save (leveraging existing --json output)
• Completion — type-aware completions for slot references, constructors, effect operations
• Go-to-definition — cross-module navigation
• Hover — display inferred types, contract annotations, effect signatures
• Find references — slot reference usage tracking

Implementation notes

Python LSP libraries (pygls, lsprotocol) provide the protocol layer. The existing compiler pipeline (parse, check, verify) already produces all the information needed — the LSP server wraps it with incremental document tracking.

Dependencies

• None (can use existing compiler pipeline)