プロトタイプ · プレビュー版：公式レジストリのすべてのサーバーを掲載し、30分ごとに同期しています。レビューとアカウント機能は今後のステップで始まります。
PopNx MCPAIを使う人のためのMCPサーバー · やさしい言葉で解説
初心者モード オフ
配色システムに合わせるライトダーク
言語ไทยEnglish中文日本語한국어EspañolDeutsch
☰ メニュー設定
初心者モード オフ
配色システムに合わせるライトダーク
言語ไทยEnglish中文日本語한국어EspañolDeutsch

MCP Z3 Prover

作者：daedalusバージョン 0.1.0i★ –iパソコンで動く
レジストリ名io.github.daedalus/mcp-z3-prover

インストール

概要

作者による説明（英語の原文）

MCP server exposing Z3 solver API

PopNx MCPの3つの柱

この3つを1つのスコアにまとめることはしません。意見、測定、人気はそれぞれ別のものだからです。

できること

このサーバーのやさしい解説はまだ書いていません。以下はレジストリから読み取った事実です。

  • 接続方法: パソコンで動く
  • トランスポート: stdio
  • カテゴリ: その他

インストール

使っているAIアプリを選んで、設定をコピーしてください。

インストールの前に

  • 基本チェック：1項目中1項目に合格
  • あなたのパソコンで、あなたのユーザーと同じ権限（ファイル、ネットワーク、アプリ）で動きます。
  • レジストリには、入力が必要なキーは載っていません。

必要なもの

  • PyPIPythonのuvのインストール（uvxコマンドに必要）

どのアプリを使っていますか？

上でアプリを選んでください。選んだアプリを覚えておくので、次からはボタンに「…にインストール」と表示されます。

Claude Desktop → Settings → Developer → Edit Config を開き、claude_desktop_config.json にこれを貼り付けます

{
  "mcpServers": {
    "z3-prover": {
      "command": "uvx",
      "args": [
        "mcp-z3-prover"
      ]
    }
  }
}

ターミナルでこれを実行します

claude mcp add z3-prover -- uvx mcp-z3-prover

Cursorで開く

または、設定を自分でコピーする

プロジェクトの .cursor/mcp.json、または ~/.cursor/mcp.json に貼り付けます

{
  "mcpServers": {
    "z3-prover": {
      "command": "uvx",
      "args": [
        "mcp-z3-prover"
      ]
    }
  }
}

ブラウザがアプリを開いてよいか確認し、そのあとアプリが設定を表示して確認を求めます。キーの値は空欄のままなので、自分で入力してください。

VS Codeで開く

または、設定を自分でコピーする

プロジェクトの .vscode/mcp.json に貼り付けます

{
  "servers": {
    "z3-prover": {
      "type": "stdio",
      "command": "uvx",
      "args": [
        "mcp-z3-prover"
      ]
    }
  }
}

ブラウザがアプリを開いてよいか確認し、そのあとアプリが設定を表示して確認を求めます。キーの値は空欄のままなので、自分で入力してください。

これはパソコンで動くサーバーですが、ChatGPTがつなげるのはインターネット上のサーバーだけです。ほかのアプリを選んでください。

選んだアプリは、この端末のCookieに保存されます。アカウントは不要です。

この設定は、作者のレジストリ登録情報から作成しています。READMEと違う場合は、READMEに従ってください。

できること

パソコンで動くサーバーです。インストールすると、ツール一覧がAIアプリに表示されます。

基本チェックi

誰でも見られる情報をチェックしており、コードは読んでいません。当てはまらない項目は数に入れていません。 · 2026年11月8日にチェック

  • ✓ 合格

    作者とリポジトリが一致

    レジストリ名は、リポジトリを所有するGitHubアカウント daedalus で確認済みです

  • … 未チェック

    今もメンテナンスされている

    このリポジトリはまだGitHubから読み取っていません

  • … 未チェック

    ライセンスがある

    このリポジトリはまだGitHubから読み取っていません

  • – 対象外

    エンドポイントが応答する

    これはパソコンで動くため、インターネット上のエンドポイントはありません

  • – 対象外

    OAuthでサインイン

    パソコンで動き、代わりにローカルの設定を使います

  • … 未チェック

    ツールの説明に隠れた指示がない

    パソコンで動くサーバーです。ツール一覧を読み取れるのは、インターネット上のエンドポイントがある場合だけです

その他のほかのサーバーとの比較i

  • このカテゴリのほかの18386件のうち0%よりスターが多い
  • このカテゴリのほかの18386件のうち4%より最近レジストリに公開
  • 基本チェックの結果が、このカテゴリのほかの18386件のうち100%と同じかそれ以上

レジストリでこのカテゴリにある有効なすべてのサーバーと比較しています。スターは、公開者がリポジトリの所有者である場合だけ数えます。

よくある質問

MCP Z3 Proverは安全ですか？

当てはまる基本チェック1項目のうち1項目に合格しました。コードは読んでいません。キーやトークンを追加する前に、サーバーがどんなアクセスを求めているかを確認し、必要な権限だけを持つキーを使ってください。

どんなキーやコードが必要ですか？

レジストリには必須のキーは載っていません。ただし、最初に使うときにサインインを求めるサーバーもあります。

パソコンで動きますか、それともクラウドですか？

あなたのパソコンで動きます。必要なときにAIアプリが起動し、データは作者のサーバーを通りません（サーバー自体がオンラインサービスを呼び出す場合を除きます）。

今もメンテナンスされていますか？

GitHubリポジトリの最終更新は–、最新バージョン（0.1.0）がレジストリに届いたのは7 か月前です。

どのアプリで使えますか？

Claude Desktop、Claude Code、Cursor、VS CodeなどのMCP対応アプリで使えます。パソコンにPython (uv)も必要です。

代わりに使えるものは？

同じカテゴリには：Spec Driven Development, Remote Desktop Commander, Tethered Trust

代わりの候補

同じカテゴリで、ほかの作者が作ったサーバー。スターの多い順。

カードの見方：★ GitHubスターi3つの柱：レビュー · チェック · 利用状況i更新＝最新バージョンをレジストリに公開した日i

Remote Desktop Commander

作者：desktop-commander

Remote Desktop Commander: use files, terminal and processes on your own computers from any AI app.

クラウドで動く★ 211一昨日更新
インストール

Tethered Trust

作者：tetheredtrust.com

Fit, compatibility and recall checks for AI agents before they buy: verdicts, evidence, receipts.

クラウドで動く今日更新
インストール

作者のREADME

READMEを開く

作者のリポジトリから書かれたとおりにコピーしたものです。PopNx MCPは内容を確認・推奨していません。HTML、画像、スクリプトは取り除いています。リンクはこのサイトの外へ移動します。

mcp-z3-prover

MCP server exposing Z3 solver API

Install

pip install mcp-z3-prover

Usage

from mcp_z3_prover import mcp

Run the server

mcp.run()

Or from command line:

mcp-z3-prover

MCP Tools

The server exposes the following tools:

  • create_bool_var - Create a Boolean variable
  • create_int_var - Create an Integer variable
  • create_real_var - Create a Real variable
  • create_int_constant - Create an integer constant
  • create_real_constant - Create a real constant
  • add_constraint - Add a constraint to the solver
  • solve - Solve the current problem
  • get_model_value - Get value of a variable from the model
  • optimize - Solve with optimization objective
  • reset_solver - Reset the solver state
  • list_variables - List all created variables

Example

# Create variables

create_int_var("x") create_int_var("y")

Add constraints

add_constraint("int:x + int:y == 10") add_constraint("int:x > 0") add_constraint("int:y > 0")

Solve

result = solve()

Returns: {"status": "sat", "model": {"x": "5", "y": "5"}}

Get specific values

x_val = get_model_value("int:x")

Integer Factorization Example
# Factor n = 4295229443 where n = p * q with q <= sqrt(n)

create_int_var("p") create_int_var("q")

Add constraints

add_constraint("int:p * int:q == 4295229443") add_constraint("4295229443 > int:p") add_constraint("4295229443 > int:q") add_constraint("int:q <= 65537") # sqrt(4295229443) ≈ 65537 add_constraint("int:q > 1") add_constraint("int:p > 1") add_constraint("int:q % 2 != 0") # q is odd add_constraint("int:p % 2 != 0") # p is odd

Solve

result = solve()

Returns: {"status": "sat", "model": {"p": "65539", "q": "65537"}}

Verification: 65537 * 65539 = 4295229443

Development

git clone https://github.com/daedalus/mcp-z3-prover.git

cd mcp-z3-prover pip install -e ".[test]"

run tests

pytest

format

ruff format src/ tests/

lint

ruff check src/ tests/

type check

mypy src/

MCP Registration

mcp-name: io.github.daedalus/mcp-z3-prover

PopNxに聞く