How do I use verso-mcp?

1. Click on "Deploy Server". 2. Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state. 3. In the chat, type @ followed by the MCP server name and your instructions, e.g., "@verso-mcp search the Lean reference for 'dependent types'" That's it! The server will respond to your query, and you can continue using it as needed. Here is a step-by-step guide with screenshots.

verso-mcp

by nvlang

Overview Schema Source Related Servers Discussions Admin

Python

Remote

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 thexref.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.

Related MCP server: devdoc

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.

Available Tools

4 tools

fetch_pageA

Read-onlyIdempotent

Fetch a page from a Verso documentation site and return it as Markdown.

Converts the site's HTML to Markdown. With an #anchor, only that single entry/section is returned (not the whole chapter). A relative path is resolved against site; an absolute URL is accepted only if it falls under a configured site root. Plain http://, off-site URLs, and path-traversal segments are rejected. Read-only.

Args: url_or_path: absolute URL on a configured site, or a site-relative path. May include an "#anchor" (e.g. ".../Tactic-Reference/#induction"). site: site to resolve a relative path against (alias from list_sites); omit for the default. Ignored when url_or_path is absolute. response_format: "markdown" (default) for the page text, or "json" for text plus metadata.

Returns: markdown: a "" header line, then the page/section as Markdown (capped at ~200 KB with a truncation marker). json: {"site","url","anchor","content","truncated"} On failure: an error string, or {"error": "..."} when response_format="json".

Examples: - Read one entry -> fetch_page(url_or_path=".../Tactic-Reference/#induction") - Read a chapter -> fetch_page(url_or_path="/Tactic-Proofs/Tactic-Reference/") - Resolve a hit -> pass the url field of a search result here.

ParametersJSON Schema

Name	Required	Description	Default
`site`	No	Which configured Verso site to use — an alias from `list_sites`. Omit to use the default site.
`url_or_path`	Yes	An absolute URL on a configured Verso site, or a site-relative path like '/Tactic-Proofs/Tactic-Reference/'. Append '#anchor' to focus on one section/entry.
`response_format`	No	'markdown' (page text) or 'json' (text + metadata)	markdown

Output Schema

ParametersJSON Schema

Name	Required	Description
`result`	Yes

TDQS

A4.6/5.0

Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

The description discloses many behavioral traits: converts HTML to Markdown, anchor handling, relative vs absolute resolution, rejection of off-site URLs and path traversal, truncation at ~200KB, and different return formats. It also states 'Read-only', matching the annotations. This adds significant context beyond the readOnly/destructive hints, such as error behavior and metadata in json mode.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is structured with clear sections (Args, Returns, Examples) and starts with a one-sentence summary. It is longer than minimal but every part adds value: parameter clarifications, return format, examples, and constraints. No filler or redundancy. Slightly verbose but justified by the tool's complexity.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

The description fully covers the tool's behavior: inputs, outputs, error handling, truncation, edge cases, and examples. It even mentions integration with search results and list_sites. Even though the input schema includes an output schema reference, the description explains the return shapes in detail, making the tool self-contained. Sibling context is well integrated.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%, so baseline is 3. The description adds meaning beyond the schema: it explains that site is used only for relative paths and ignored for absolute URLs, that anchors focus on a section, and that url_or_path can be an absolute URL on a configured site or a site-relative path. It also clarifies the response_format options and their payloads, exceeding what the schema states.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description opens with a specific verb and resource: 'Fetch a page from a Verso documentation site and return it as Markdown.' It clearly distinguishes from siblings by explaining it fetches page content, while list_sites lists sites, list_kinds lists kinds, and search finds content. The scope (single page/section with anchor) is also stated.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly instructs when to use the tool: to read a chapter, a single entry via #anchor, or resolve a search hit. It references list_sites for the site alias and search for passing the url field, showing context. It does not explicitly say 'when not to use' but the URL constraints and examples imply alternatives. This is clear guidance, though not as explicit as naming an alternative tool.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

list_kindsA

Read-onlyIdempotent

List the kinds of entries indexed for a Verso site, with counts.

Kinds are derived from the site's cross-reference index — they vary per site (a language reference has tactics and options; a textbook has sections and terms). Use the returned kind values to filter search. Read-only.

Args: site: which configured site (alias from list_sites); omit for the default. response_format: "markdown" (default) or "json".

Returns: markdown: a table of kind, count, and human-readable description. json: {"site": str, "root": str, "total_entries": int, "kinds": [{"kind","count","description"}, ...]}

ParametersJSON Schema

Name	Required	Description	Default
`site`	No	Which configured Verso site to use — an alias from `list_sites`. Omit to use the default site.
`response_format`	No	'markdown' (human-readable) or 'json' (structured)	markdown

Output Schema

ParametersJSON Schema

Name	Required	Description
`result`	Yes

TDQS

A4.5/5.0

Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already cover read-only/idempotent behavior. The description adds meaningful context beyond that: kinds derive from the site's cross-reference index, vary per site, and the return shape for both markdown and JSON is fully documented. It does not contradict any annotation.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is well-structured: a concise opening definition, a brief explanatory paragraph about site variability and usage, then clearly formatted Args and Returns sections. Every sentence adds value, and there is no unnecessary verbosity.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

The tool is simple and well-covered: annotations declare safety, the description details what kinds are, how they relate to sites, how to use the output with `search`, and the exact return formats for both markdown and JSON. This is complete for an agent to select and invoke correctly.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%, so the schema already documents both parameters. The description's Args section restates the same information (site alias, response_format options) without adding new meaning. This meets the baseline for high schema coverage.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The opening sentence states a specific action ('List') and resource ('kinds of entries') with the scope of a Verso site and counts. It clearly distinguishes itself from siblings by explaining that the returned kind values are used to filter `search`, and it references `list_sites` for site aliases.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines5/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly tells the agent when to use this tool: to obtain `kind` values for filtering `search`. It also explains that kinds vary per site, implying the tool is needed to discover them dynamically. This is an explicit use case with a named alternative (`search`).

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

list_sitesA

Read-onlyIdempotent

List the Verso documentation sites this server is configured to serve.

Each site has an alias — pass it as the site argument to search, list_kinds, or fetch_page to target that site. Sites are configured via the VERSO_MCP_SITES environment variable. Read-only.

Args: response_format: "markdown" (default) or "json".

Returns: markdown: one line per site (alias, default marker, root URL). json: {"default": str, "sites": [{"alias","root","indexed"}, ...]}

ParametersJSON Schema

Name	Required	Description	Default
`response_format`	No	'markdown' (human-readable) or 'json' (structured)	markdown

Output Schema

ParametersJSON Schema

Name	Required	Description
`result`	Yes

TDQS

A4.9/5.0

Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Beyond the annotations (readOnlyHint, idempotentHint, destructiveHint), the description adds significant behavioral detail: it specifies the exact return format for both markdown and JSON, including the structure of the JSON object. It also discloses that sites are configured via an environment variable, which is context not available in the annotations.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is well-structured with a clear intent, relationship to siblings, configuration note, and Args/Returns sections. Every sentence contributes essential information, and it is front-loaded with the primary purpose.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

For a simple listing tool, the description is fully self-sufficient: it covers purpose, usage, configuration, parameters, and return formats. The relationship to sibling tools is explicitly stated, and the presence of an output schema further enriches the context. No gaps remain for the agent to guess.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The schema fully documents the `response_format` parameter with an enum and default. The description goes beyond by explaining concretely what each format returns (line-by-line markdown vs. structured JSON with a default site and sites list), helping the agent choose the right format. This adds value beyond the schema's generic description.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool lists Verso documentation sites the server is configured to serve, using the verb 'List' and a specific resource. It also distinguishes itself from siblings by explaining how each site's alias is used as the `site` argument in `search`, `list_kinds`, and `fetch_page`.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines5/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly explains that the returned aliases should be passed to sibling tools, providing concrete usage instructions. It also mentions configuration via `VERSO_MCP_SITES`, giving the agent context for how sites are populated and when to expect them.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

searchA

Read-onlyIdempotent

Search a Verso documentation site's cross-reference index by name.

Matches entry names and display names (not free text inside pages — use fetch_page to read a page). Results are ranked by match quality and paginated. Read-only.

Args: query: free-text query matched against canonical and user-facing names. site: which configured site (alias from list_sites); omit for the default. kind: optional kind filter — one of the values from list_kinds. limit: maximum results per page, 1-100 (default 20). offset: number of results to skip, for pagination (default 0). response_format: "markdown" (default) or "json".

Returns: markdown: a header ("N matches … showing X-Y") then one bullet per hit ("- [kind] display — url"), plus a hint to re-call with a higher offset. json: {"site","query","kind","total","count","offset","has_more", "next_offset","results":[{"kind","name","display","url",...}]}

Examples: - "Find the simp tactic" -> search(query="simp", kind="tactic") - "Search the FPiL book for monads" -> search(query="monad", site="fpil") - "Next page of results" -> search(query=..., offset=20)

ParametersJSON Schema

Name	Required	Description	Default
`kind`	No	Optional kind filter from `list_kinds` (e.g. 'tactic', 'section', 'option').
`site`	No	Which configured Verso site to use — an alias from `list_sites`. Omit to use the default site.
`limit`	No	Maximum results per page.
`query`	Yes	Free-text query, matched against canonical and display names (e.g. 'simp', 'Nat.add', 'monad').
`offset`	No	Number of results to skip, for pagination.
`response_format`	No	'markdown' (human-readable) or 'json' (structured)	markdown

Output Schema

ParametersJSON Schema

Name	Required	Description
`result`	Yes

TDQS

A4.9/5.0

Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Beyond the annotations (readOnlyHint, idempotentHint, etc.), the description discloses that results are 'ranked by match quality and paginated,' and explains the behavior for pagination via offset and the hint to re-call with a higher offset. It also details return formats and what fields are included.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is well-structured with clear sections (main description, Args, Returns, Examples). Every sentence contributes useful information, and the use of labeled sections improves readability without unnecessary fluff.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the tool's complexity (6 parameters, multiple response formats, pagination) and rich schema/annotations, the description fully covers all aspects: what it searches, how to filter, pagination behavior, return formats, and examples. No significant gaps remain.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The schema covers all parameters with descriptions (100% coverage), so the baseline is 3. The description adds value through concrete examples mapping natural language ('Find the simp tactic') to parameter combinations, which helps the agent select correct arguments. However, the Args section itself largely paraphrases the schema.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description states a specific verb and resource: 'Search a Verso documentation site's cross-reference index by name.' It clearly distinguishes itself from sibling tools by noting that it does not search free text inside pages, for which `fetch_page` is the intended alternative.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines5/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly gives usage context: 'Matches entry names and display names (not free text inside pages — use `fetch_page` to read a page).' It also references sibling tools `list_sites` and `list_kinds` for valid site and kind values, and provides examples of when to use the tool.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Tool Schema Changelog

Recent tool additions, removals, and schema changes observed during successful MCP inspections.

4 tool updatesv0.1.0Aug 5, 2026
- First observedfetch_page
- First observedlist_kinds
- First observedlist_sites
- First observedsearch

Deploy Server

One endpoint for every MCP toolRayrun runs every MCP server behind one URL and holds the credentials. Each call is decided per client, tool, and argument, then recorded.ray.runAd

TDQS

A4.7/5.0

Scored 2026-08-05 07:10 across 4 tools

Disambiguation5/5

Each tool has a distinct purpose: listing sites, listing kinds, searching, and fetching pages. No overlap or ambiguity; they form a clear progression from discovery to retrieval.

Naming Consistency5/5

All tool names follow a consistent verb-based pattern with underscores: list_sites, list_kinds, search, fetch_page. The naming is predictable and readable.

Tool Count5/5

Four tools is well-scoped for a documentation querying server. Each tool is necessary and none are redundant.

Completeness5/5

The tool surface covers the full read-only workflow: discover sites, explore index structure, search entries, and fetch page content. No obvious gaps for the stated purpose.

Maintenance

ActivityMaintained

ResponsivenessNo issues

Resources

Need Help?

Related Servers

Related MCP Connectors

agentverse
io.github.doc2mcp
MCP server for agentverse documentation, generated by doc2mcp.
Agent Orchestration Documentation Access
24
gread A
io.github.NitroRCr
An MCP server that gives your AI access to the source code and docs of all public github repos
Version Control Code Analysis Documentation Access
5361
Knowa
com.knowalabs
Team docs served to AI agents over MCP - search, Markdown reads, version pinning, read audit.
Documentation Access Knowledge & Memory Search
2
forkast-mcp-docs A
io.github.ForkastPredict
MCP server for querying Forkast documentation
Documentation Access Search Developer Tools
42

Related MCP Servers

mcp-docs
Documentation Access Search
gmantovani2005
A
license
Not graded
quality
C
maintenance
Generic MCP server that exposes Markdown documentation to LLMs, enabling them to search and answer questions about any software documentation.
Updated 4 months ago (2026-05-03 13:02 UTC)
MIT
devdoc
Documentation Access RAG Systems Search
vision-release
A
license
Not graded
quality
B
maintenance
A documentation MCP server that crawls websites and Git repositories, stores them as Markdown, and provides tools to search and retrieve documentation for local LLMs and AI agents.
Updated 5 months ago (2026-04-10 16:44 UTC)
Apache 2.0
Docs MCP
Web Scraping Documentation Access Search
Ruoth1111
F
license
A
quality
C
maintenance
An MCP server that searches official documentation for popular libraries, scrapes pages, and returns clean, LLM-ready text.
Updated 3 months ago (2026-06-27 15:59 UTC)
1
-
docs-mcp-server
Documentation Access Developer Tools
DewminK
F
license
Not graded
quality
B
maintenance
MCP server that exposes one or more documentation folders (Markdown, MDX, TXT) to AI agents, enabling listing, reading, and searching of documentation files.
Updated 2 months ago (2026-07-11 20:48 UTC)
-