Verso Mcp 100/100 — SaferSkills

Is Verso Mcp safe to install?

SaferSkills independently audited Verso Mcp (Agent Skill) and scored it 100/100 (green). The audit ran 55 deterministic rules across Security, Supply Chain, Maintenance, Transparency, and Community; it found 0 high-severity and 0 lower-severity findings. The full rule-by-rule trace and per-finding evidence are below. Free, methodology-open.

CategoryWeightCategory scoreContribution

Securityprompt, exec, net, exfil, eval

35%

100

35.0 pts

Supply chainhash, typosquat, maintainer, lockfile

20%

100

20.0 pts

Maintenancestaleness, pinning, CI

15%

100

15.0 pts

TransparencySKILL.md, perms, README

15%

100

15.0 pts

Communityinstalls, verify, response

15%

100

15.0 pts

Findings & checks · 0 flagged

Securityscore 100 · 0 findings

✓—All security checks passedNo findings in this category for the latest scan.pass

Supply chainscore 100 · 0 findings

✓—All supply chain checks passedNo findings in this category for the latest scan.pass

Maintenancescore 100 · 0 findings

✓—All maintenance checks passedNo findings in this category for the latest scan.pass

Transparencyscore 100 · 0 findings

✓—All transparency checks passedNo findings in this category for the latest scan.pass

Communityscore 100 · 0 findings

✓—All community checks passedNo findings in this category for the latest scan.pass

The primary manifest — the file an agent reads to learn what this artifact does.

README.md · 1 file

README.md10.0 KB · Markdown

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

Verso Mcp— agent skill

Is Verso Mcp safe to install?

Tools

Configuring sites

Requirements

Use with Claude Code / Claude Desktop

Environment variables

Safety & etiquette

Evaluation

Limitations

Disclaimer

Audit the pieces. Scan the whole. Decide.