\n \n \n\nAn [MCP](https://modelcontextprotocol.io) (Model Context Protocol) server that\nlets an AI agent search and read documentation built with\n[Verso](https://github.com/leanprover/verso), Lean's documentation authoring\ntool.\n\nVerso powers most of the Lean ecosystem's reference docs and books — the\n[Lean Language Reference](https://lean-lang.org/doc/reference/latest/),\n[Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/),\n[Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/),\nand more. Verso *Manual*-genre sites publish a machine-readable cross-reference\nindex (`xref.json`); this server consumes that index and the rendered HTML.\n\n> [!WARNING]\n> The format of the `xref.json` files that this server depends on is\n> Verso-internal and may change at any time. Such changes could render this\n> server non-functional. I'll try to keep up with any such changes, but can't\n> make any promises.\n\nPoint it at one or more Verso sites and an agent gets four read-only tools:\n`list_sites`, `list_kinds`, `search`, and `fetch_page`.\n\n## Tools\n\n| Tool | Description |\n| ------------ | ------------------------------------------------------------------------------------------------- |\n| `list_sites` | Enumerate the configured Verso sites and their aliases. |\n| `list_kinds` | List a site's entry kinds (tactics, terms, sections, options, …) with counts. |\n| `search` | Name-ranked search over a site's cross-reference index, with `kind` filtering and pagination. |\n| `fetch_page` | Fetch a page — or a single `#anchor` entry — from a site and return it as Markdown. |\n\n`list_kinds`, `search`, and `fetch_page` take an optional `site` argument (an\nalias from `list_sites`); omit it to use the default site. All tools are\nread-only and accept a `response_format` of `markdown` (default) or `json`.\n\nEntry \"kinds\" are derived dynamically from each site's `xref.json`, so\nproject-specific domains (Lake commands, error explanations, …) are picked up\nautomatically — nothing about a particular site is hard-coded.\n\n## Configuring sites\n\nSet the `VERSO_MCP_SITES` environment variable to a comma-separated list of\n`alias=url` pairs. A bare URL (no `alias=`) gets an alias derived from its path.\n\n```\nVERSO_MCP_SITES=\"lean-reference=https://lean-lang.org/doc/reference/latest/,\n fpil=https://lean-lang.org/functional_programming_in_lean/,\n tpil=https://lean-lang.org/theorem_proving_in_lean4/\"\n```\n\nThe first site listed is the default. If `VERSO_MCP_SITES` is unset, the server\ndefaults to a single site, the Lean Language Reference.\n\nA site URL must be the root directory that contains `xref.json` (Verso writes it\nthere for Manual- and Tutorial-genre sites). The configured site roots also\nserve as the network allowlist — see [Safety](#safety--etiquette).\n\n## Requirements\n\n[uv](https://docs.astral.sh/uv/). `uv` fetches the package and its dependencies\nautomatically on first launch — no manual virtualenv or `pip install` step.\n\n## Use with Claude Code / Claude Desktop\n\nAdd an entry to your MCP configuration (`.mcp.json`, `~/.claude.json`, or\n`claude_desktop_config.json`):\n\n```json\n{\n \"mcpServers\": {\n \"verso\": {\n \"type\": \"stdio\",\n \"command\": \"uvx\",\n \"args\": [\"verso-mcp\"],\n \"env\": {\n \"VERSO_MCP_SITES\": \"lean-reference=https://lean-lang.org/doc/reference/latest/, fpil=https://lean-lang.org/functional_programming_in_lean/\"\n }\n }\n }\n}\n```\n\n## Environment variables\n\nAll optional:\n\n| Variable | Default | Purpose |\n| --------------------------- | ----------------------------- | ---------------------------------------------------------------- |\n| `VERSO_MCP_SITES` | Lean Language Reference | Comma-separated `alias=url` site list (see above). |\n| `VERSO_MCP_CACHE` | `~/.cache/verso-mcp` | Cache directory (each site cached in its own subdirectory). |\n| `VERSO_MCP_RATE_PER_SEC` | `2` | Sustained outbound request rate (requests/second). |\n| `VERSO_MCP_RATE_BURST` | `5` | Token-bucket burst capacity. |\n| `VERSO_MCP_RATE_MAX_WAIT` | `3` | Max seconds to wait for a token before refusing. |\n\n## Safety & etiquette\n\n> [!WARNING]\n> [MCP servers have a lot of\n> risks](https://www.redhat.com/en/blog/model-context-protocol-mcp-understanding-security-risks-and-controls).\n> As far as MCP servers go, this one (`verso-mcp`) should be relatively\n> innocuous: it is read-only, runs no shell commands, and only reaches the\n> documentation sites you configure (or just the Lean Language Reference, if\n> left unconfigured). The main caveat is that a malicious or compromised\n> documentation site could try to steer the model via indirect prompt injection.\n> `verso-mcp` cannot prevent that, so don't let an agent that uses it take\n> consequential actions without your review.\n\nThe server is built to be a well-behaved client of documentation sites:\n\n- **Scoped network access** — fetches are restricted to the *configured site\n roots*; the site list doubles as the allowlist. Enforced on the request URL\n *and* the final post-redirect URL, so a same-host URL outside a configured\n root is still refused. Path traversal (`..`, `%2e%2e`, backslash variants) is\n rejected.\n- **Obeys `robots.txt`** — each host's `robots.txt` is fetched and respected\n for this server's `User-Agent`; a host can target it specifically with a\n `User-agent: verso-mcp` group.\n- **Rate limiting** — a shared token bucket caps outbound requests across all\n sites (default 2 req/s, burst 5); a hit falls back to cached content rather\n than hammering the origin.\n- **Caching & revalidation** — `xref.json` and pages are cached on disk per\n site (24 h TTL) with `ETag`/`If-None-Match` conditional revalidation, so a\n repeated lookup costs at most a `304 Not Modified`.\n- **Bounded responses** — HTTP bodies are streamed with an 8 MB cap; Markdown\n output is capped at 200 KB; each site's page cache is LRU-evicted at 200 MB.\n- **Identifying `User-Agent`** on every request.\n\n## Evaluation\n\n`evaluation.xml` is a 10-question evaluation suite in the format used by\nAnthropic's `mcp-builder` skill. The questions target the default site (the\nLean Language Reference); each is read-only, independent, and has a single\nstable, verifiable answer.\n\n## Limitations\n\n- Works with Verso **Manual**-genre sites (those that publish `xref.json`).\n Blog-genre sites have no `xref.json`. Tutorial-genre sites also emit one and\n should work, but are untested.\n- `search` is **name-based** — it matches entry names and titles in the\n cross-reference index, the same granularity as Verso's own on-site search. It\n does not do full-text search of page bodies.\n- The `xref.json` schema is an undocumented Verso internal; it may shift between\n Verso releases, which could break this MCP server if it doesn't keep up.\n\n## Disclaimer\n\nThis project was written almost entirely by\n[Claude Opus 4.7 (1M)](https://www.anthropic.com/news/claude-opus-4-7), an AI\nassistant. It was built for my own personal use and is shared here only in case\nit is useful to others. It comes with **no warranty whatsoever**. Use it at your\nown risk.\n\n\n",
"bytes": 10188,
"sha": "646bd6a60d23f6970ed8793d947113419576b0c84b31efd39422ffdaa7b6d688",
"repo_slug": "nvlang/verso-mcp",
"fonte": "repo",
"truncated": false,
"api": "https://agentalog.com/api/listings/mcp_io_github_nvlang_verso_55a069e6/readme"
}
![\"verso-mcp\"](\"https://raw.githubusercontent.com/nvlang/verso-mcp/main/res/logotype-light.svg\")
\n![\"PyPI](\"https://img.shields.io/pypi/v/verso-mcp?style=flat-square&logo=pypi&logoColor=24292f&label=&labelColor=eaeef2&color=eaeef2\")
![\"Supported](\"https://img.shields.io/badge/dynamic/json?url=https%3A%2F%2Fpypi.org%2Fpypi%2Fverso-mcp%2Fjson&query=%24.info.requires_python&style=flat-square&logo=python&logoColor=24292f&label=&labelColor=eaeef2&color=eaeef2\")
![\"OpenSSF](\"https://img.shields.io/ossf-scorecard/github.com/nvlang/verso-mcp?style=flat-square&labelColor=eaeef2&color=eaeef2&label=OpenSSF%20Scorecard\")