MCP Servers

verso-mcp

An MCP server that lets AI agents search and read documentation built with Verso, Lean's documentation authoring tool, by providing tools like search and fetch_page over configured documentation sites.

README

</div> </div> <br> <br>

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

Tool	Description
`list_sites`	Enumerate the configured Verso sites and their aliases.
`list_kinds`	List a site's entry kinds (tactics, terms, sections, options, …) with counts.
`search`	Name-ranked search over a site's cross-reference index, with `kind` filtering and pagination.
`fetch_page`	Fetch a page — or a single `#anchor` entry — from a site and return it as Markdown.

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:

Variable	Default	Purpose
`VERSO_MCP_SITES`	Lean Language Reference	Comma-separated `alias=url` site list (see above).
`VERSO_MCP_CACHE`	`~/.cache/verso-mcp`	Cache directory (each site cached in its own subdirectory).
`VERSO_MCP_RATE_PER_SEC`	`2`	Sustained outbound request rate (requests/second).
`VERSO_MCP_RATE_BURST`	`5`	Token-bucket burst capacity.
`VERSO_MCP_RATE_MAX_WAIT`	`3`	Max seconds to wait for a token before refusing.

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

This project was written almost entirely by Claude Opus 4.7 (1M), an AI assistant. It was built for my own personal use and is shared here only in case it is useful to others. It comes with no warranty whatsoever. Use it at your own risk.

Recommended Servers

playwright-mcp

A Model Context Protocol server that enables LLMs to interact with web pages through structured accessibility snapshots without requiring vision models or screenshots.

Official

Featured

TypeScript

Audiense Insights MCP Server

Enables interaction with Audiense Insights accounts via the Model Context Protocol, facilitating the extraction and analysis of marketing insights and audience data including demographics, behavior, and influencer engagement.

Magic Component Platform (MCP)

An AI-powered tool that generates modern UI components from natural language descriptions, integrating with popular IDEs to streamline UI development workflow.

VeyraX MCP

Single MCP tool to connect all your favorite tools: Gmail, Calendar and 40 more.

Official

Featured

Local

graphlit-mcp-server

The Model Context Protocol (MCP) Server enables integration between MCP clients and the Graphlit service. Ingest anything from Slack to Gmail to podcast feeds, in addition to web crawling, into a Graphlit project - and then retrieve relevant contents from the MCP client.

Official

Featured

TypeScript

Kagi MCP Server

An MCP server that integrates Kagi search capabilities with Claude AI, enabling Claude to perform real-time web searches when answering questions that require up-to-date information.

Official

Featured

Python

E2B

Using MCP to run code via e2b.

Official

Featured

Neon Database

MCP server for interacting with Neon Management API and databases

Official

Featured

Exa Search

A Model Context Protocol (MCP) server lets AI assistants like Claude use the Exa AI Search API for web searches. This setup allows AI models to get real-time web information in a safe and controlled way.

Official

Featured

Qdrant Server

This repository is an example of how to create a MCP server for Qdrant, a vector search engine.

Official

Featured