verso

Verso（Lean のドキュメント作成ツール）で構築されたドキュメントを、AI エージェントが検索・閲覧できる MCP（Model Context Protocol）サーバーです。

Verso は Lean エコシステムのリファレンスドキュメントや書籍の大部分を支えています。たとえば、Lean Language Reference、Functional Programming in Lean、Theorem Proving in Lean 4 などがあります。Verso の Manual ジャンルのサイトでは、機械可読な相互参照インデックス（xref.json）が公開されます。このサーバーはそのインデックスとレンダリング済み HTML を利用します。

警告

このサーバーが依存する xref.json ファイルの形式は Verso 内部のものであり、予告なく変更される可能性があります。そのような変更により、このサーバーが動作しなくなることがあります。変更には対応するよう努めますが、対応を保証することはできません。

1 つ以上の Verso サイトを指定すると、エージェントは読み取り専用の 4 つのツール、list_sites、list_kinds、search、fetch_page を利用できます。

ツール

ツール	説明
list_sites	設定されている Verso サイトとそのエイリアスを列挙します。
list_kinds	サイトのエントリー種別（tactics、terms、sections、options、…）を件数とともに一覧表示します。
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 の組をカンマ区切りで設定します。 alias= のない URL には、そのパスから導出されたエイリアスが割り当てられます。

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）は比較的 無害なはずです。読み取り専用で、シェルコマンドを実行せず、設定した ドキュメントサイト（未設定の場合は Lean Language Reference のみ）にしか アクセスしません。主な注意点は、悪意のある、または侵害された ドキュメントサイトが間接的なプロンプトインジェクションを通じてモデルを 誘導しようとする可能性があることです。verso-mcp ではこれを防げないため、 これを使用するエージェントに、レビューなしで重大な結果を伴う操作を 実行させないでください。

このサーバーは、ドキュメントサイトに対して適切に振る舞うクライアントとなるよう構築されています。

• 範囲を限定したネットワークアクセス — フェッチ先は設定されたサイトのルートに制限されます。サイトリストは許可リストも兼ねます。リクエスト URL とリダイレクト後の最終 URL の両方で制限を適用するため、同じホストでも設定されたルート外の URL は拒否されます。パストラバーサル（..、%2e%2e、バックスラッシュの亜種）は拒否されます。
• robots.txt に従います — 各ホストの robots.txt を取得し、このサーバーの User-Agent に適用されるルールに従います。ホスト側では User-agent: verso-mcp グループを使って個別に指定できます。
• レート制限 — 共有トークンバケットにより、すべてのサイトへの送信リクエスト数を制限します（デフォルトは 2 req/s、バーストは 5）。制限に達すると、オリジンサーバーに過剰なリクエストを送る代わりに、キャッシュされたコンテンツを使用します。
• キャッシュと再検証 — xref.json とページはサイトごとにディスクへキャッシュされ（TTL は 24 h）、ETag／If-None-Match による条件付き再検証を行います。そのため、同じ検索を繰り返しても、リクエストは最大で 304 Not Modified になります。
• レスポンスの上限 — HTTP ボディはストリーミングで取得し、上限を 8 MB に設定します。Markdown 出力の上限は 200 KB です。各サイトのページキャッシュは 200 MB で LRU 方式により削除されます。
• すべてのリクエストで User-Agent を明示します。

評価

evaluation.xml は、Anthropic の mcp-builder スキルで使われている形式の 10 問からなる評価スイートです。質問はデフォルトのサイト（Lean Language Reference）を対象としており、どれも読み取り専用で、互いに独立していて、安定して検証可能な回答が 1 つあります。

制限事項

• Verso の Manual ジャンルのサイト（xref.json を公開しているサイト）で動作します。Blog ジャンルのサイトには xref.json がありません。Tutorial ジャンルのサイトも xref.json を出力するため動作するはずですが、テストはされていません。
• search は名前ベースです。クロスリファレンスインデックス内のエントリー名とタイトルを対象に検索します。これは Verso 独自のサイト内検索と同じ粒度です。ページ本文の全文検索は行いません。
• xref.json のスキーマは、文書化されていない Verso の内部仕様です。Verso のリリース間で変更される可能性があり、追従できない場合、この MCP サーバーが動作しなくなることがあります。

免責事項

このプロジェクトは、ほぼすべて Claude Opus 4.7 (1M) という AI アシスタントによって作成されました。個人利用のために構築したもので、ほかの方の 役に立つ場合に備えてここで共有しています。いかなる保証もありません。ご自身の 責任でご利用ください。