Verso

An MCP (Model Context Protocol) server that lets an AI agent search and read documentation built with Verso, Lean's documentation authoring tool.

Verso powers most of the Lean ecosystem's reference docs and books — the Lean Language Reference, Functional Programming in Lean, Theorem Proving in Lean 4, and more. Verso Manual-genre sites publish a machine-readable cross-reference index (xref.json); this server consumes that index and the rendered HTML.

[!WARNING] The format of the xref.json files that this server depends on is Verso-internal and may change at any time. Such changes could render this server non-functional. I'll try to keep up with any such changes, but can't make any promises.

Point it at one or more Verso sites and an agent gets four read-only tools: list_sites, list_kinds, search, and fetch_page.

Tools

list_kinds, search, and fetch_page take an optional site argument (an alias from list_sites); omit it to use the default site. All tools are read-only and accept a response_format of markdown (default) or json.

Entry "kinds" are derived dynamically from each site's xref.json, so project-specific domains (Lake commands, error explanations, …) are picked up automatically — nothing about a particular site is hard-coded.

Configuring sites

Set the VERSO_MCP_SITES environment variable to a comma-separated list of alias=url pairs. A bare URL (no alias=) gets an alias derived from its path.

VERSO_MCP_SITES="lean-reference=https://lean-lang.org/doc/reference/latest/,
                 fpil=https://lean-lang.org/functional_programming_in_lean/,
                 tpil=https://lean-lang.org/theorem_proving_in_lean4/"

The first site listed is the default. If VERSO_MCP_SITES is unset, the server defaults to a single site, the Lean Language Reference.

A site URL must be the root directory that contains xref.json (Verso writes it there for Manual- and Tutorial-genre sites). The configured site roots also serve as the network allowlist — see Safety.

Requirements

uv. uv fetches the package and its dependencies automatically on first launch — no manual virtualenv or pip install step.

Use with Claude Code / Claude Desktop

Add an entry to your MCP configuration (.mcp.json, ~/.claude.json, or claude_desktop_config.json):

{
  "mcpServers": {
    "verso": {
      "type": "stdio",
      "command": "uvx",
      "args": ["verso-mcp"],
      "env": {
        "VERSO_MCP_SITES": "lean-reference=https://lean-lang.org/doc/reference/latest/, fpil=https://lean-lang.org/functional_programming_in_lean/"
      }
    }
  }
}

Environment variables

All optional:

Safety & etiquette

[!WARNING] MCP servers have a lot of risks. As far as MCP servers go, this one (verso-mcp) should be relatively innocuous: it is read-only, runs no shell commands, and only reaches the documentation sites you configure (or just the Lean Language Reference, if left unconfigured). The main caveat is that a malicious or compromised documentation site could try to steer the model via indirect prompt injection. verso-mcp cannot prevent that, so don't let an agent that uses it take consequential actions without your review.

The server is built to be a well-behaved client of documentation sites:

• Scoped network access — fetches are restricted to the configured site roots; the site list doubles as the allowlist. Enforced on the request URL and the final post-redirect URL, so a same-host URL outside a configured root is still refused. Path traversal (.., %2e%2e, backslash variants) is rejected.
• Obeys robots.txt — each host's robots.txt is fetched and respected for this server's User-Agent; a host can target it specifically with a User-agent: verso-mcp group.
• Rate limiting — a shared token bucket caps outbound requests across all sites (default 2 req/s, burst 5); a hit falls back to cached content rather than hammering the origin.
• Caching & revalidation — xref.json and pages are cached on disk per site (24 h TTL) with ETag/If-None-Match conditional revalidation, so a repeated lookup costs at most a 304 Not Modified.
• Bounded responses — HTTP bodies are streamed with an 8 MB cap; Markdown output is capped at 200 KB; each site's page cache is LRU-evicted at 200 MB.
• Identifying User-Agent on every request.

Evaluation

evaluation.xml is a 10-question evaluation suite in the format used by Anthropic's mcp-builder skill. The questions target the default site (the Lean Language Reference); each is read-only, independent, and has a single stable, verifiable answer.

Limitations

• Works with Verso Manual-genre sites (those that publish xref.json). Blog-genre sites have no xref.json. Tutorial-genre sites also emit one and should work, but are untested.
• search is name-based — it matches entry names and titles in the cross-reference index, the same granularity as Verso's own on-site search. It does not do full-text search of page bodies.
• The xref.json schema is an undocumented Verso internal; it may shift between Verso releases, which could break this MCP server if it doesn't keep up.

Disclaimer