verso

一个 MCP（模型上下文协议）服务，可让 AI Agent 搜索和阅读使用 Verso（Lean 的文档编写工具）构建的文档。

Verso 为 Lean 生态系统中的大多数参考文档和书籍提供支持，包括 Lean 语言参考、Lean 函数式编程、Lean 4 定理证明等。Verso Manual 体裁的网站会发布机器可读的交叉引用索引（xref.json）；此服务会读取该索引和渲染后的 HTML。

警告

此服务依赖的 xref.json 文件格式属于 Verso 内部格式，随时可能发生变化。这类变化可能导致此服务无法运行。我会尽力跟进此类变化，但无法作出任何保证。

将一个或多个 Verso 网站作为目标后，Agent 就能使用四种只读工具：list_sites、list_kinds、search 和 fetch_page。

工具

工具	描述
list_sites	列出已配置的 Verso 站点及其别名。
list_kinds	列出站点的条目类型（策略、术语、章节、选项等）及其数量。
search	在站点的交叉引用索引中按名称排序搜索，支持按 kind 筛选和分页。
fetch_page	获取页面或单个 #anchor 条目，并以 Markdown 格式返回。

list_kinds、search 和 fetch_page 接受可选的 site 参数（来自 list_sites 的别名）；省略该参数则使用默认站点。所有工具均为只读，并接受 markdown（默认值）或 json 格式的 response_format。

条目“类型”会根据各站点的 xref.json 动态生成，因此会自动识别特定项目的领域 （Lake 命令、错误说明等），无需对任何特定站点进行硬编码。

配置站点

将 VERSO_MCP_SITES 环境变量设置为以逗号分隔的 alias=url 键值对列表。若只提供 URL（不含 alias=），则会根据其路径生成别名。

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

列表中的第一个站点为默认站点。如果未设置 VERSO_MCP_SITES，服务将默认使用单个站点，即 Lean Language Reference。

站点 URL 必须指向包含 xref.json 的根目录（Verso 会为 Manual 和 Tutorial 类型的站点在此处写入该文件）。配置的站点根目录也用作网络允许列表，详见安全与礼仪。

要求

uv。uv 会在首次启动时自动获取软件包及其依赖项，无需手动创建虚拟环境或执行 pip install。

与 Claude Code / Claude Desktop 搭配使用

在 MCP 配置文件（.mcp.json、~/.claude.json 或 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/"
      }
    }
  }
}

环境变量

均为可选项：

变量	默认值	用途
VERSO_MCP_SITES	Lean Language Reference	以逗号分隔的 alias=url 站点列表（见上文）。
VERSO_MCP_CACHE	~/.cache/verso-mcp	缓存目录（每个站点缓存在各自的子目录中）。
VERSO_MCP_RATE_PER_SEC	2	持续的出站请求速率（请求/秒）。
VERSO_MCP_RATE_BURST	5	令牌桶突发容量。
VERSO_MCP_RATE_MAX_WAIT	3	拒绝请求前等待令牌的最长秒数。

安全与礼仪

警告

MCP 服务存在许多 风险。 就 MCP 服务而言，这个服务（verso-mcp）应该相对 无害：它是只读的，不会运行 shell 命令，并且只会访问你配置的 文档网站（如果未配置，则只访问 Lean 语言参考）。主要需要注意的是， 恶意或遭到入侵的文档网站可能会试图通过间接提示词注入来引导模型。 verso-mcp 无法阻止这种情况，因此，使用它的 Agent 在未经过你审查的情况下， 不应采取会造成重大影响的操作。

此服务旨在成为文档网站的守规客户端：

• 限定网络访问范围 — 抓取范围仅限于已配置的网站根路径；网站列表同时充当允许列表。请求 URL 和重定向后的最终 URL 都会受到限制，因此，即使是同一主机上位于已配置根路径之外的 URL，也会被拒绝。路径遍历（..、%2e%2e、反斜杠变体）会被拒绝。
• 遵守 robots.txt — 获取每个主机的 robots.txt，并遵守其中针对本服务 User-Agent 的规则；主机可以使用 User-agent: verso-mcp 规则组专门针对本服务。
• 速率限制 — 共享令牌桶会限制所有网站的出站请求（默认每秒 2 次请求，突发上限为 5 次）；达到限制时，会使用缓存内容，而不会不断请求源站。
• 缓存与重新验证 — xref.json 和页面会按网站缓存在磁盘上（TTL 为 24 小时），并通过 ETag/If-None-Match 进行条件重新验证，因此重复查询最多只会产生一次 304 Not Modified 响应。
• 限制响应大小 — HTTP 响应正文以流式方式读取，上限为 8 MB；Markdown 输出上限为 200 KB；每个网站的页面缓存达到 200 MB 时会按 LRU 策略淘汰。
• 每次请求都会使用可识别的 User-Agent。

评估

evaluation.xml 是一个包含 10 个问题的评估套件，采用 Anthropic 的 mcp-builder 技能所用的格式。这些问题针对默认网站（Lean 语言参考）；每个问题均为只读、相互独立，并且只有一个稳定且可验证的答案。

限制

• 适用于 Verso Manual 类型的网站（会发布 xref.json 的网站）。Blog 类型的网站没有 xref.json。Tutorial 类型的网站也会生成该文件，理论上应该适用，但尚未经过测试。
• search 基于名称 — 它会在交叉引用索引中匹配条目名称和标题，粒度与 Verso 自身的网站内搜索相同。它不会对页面正文进行全文搜索。
• xref.json 的架构是未公开文档的 Verso 内部实现；它可能会随 Verso 版本发布而变化，如果本 MCP 服务未能及时跟进，就可能导致服务无法正常工作。

免责声明

本项目几乎完全由 Claude Opus 4.7 (1M) 这一 AI 助手编写。它是为我个人使用而构建的，仅在可能对他人有用时才在此分享。不提供任何保证。使用风险由你自行承担。