MCP Z3 Prover

MCP server exposing Z3 solver API

Quick Install

Automated & IDE Setup

Copy the AI prompt to install this server into Claude Code, Cursor, or another agent — or use 1-click editor setup below.

Add to Cursor Add to VS Code

Not yet automatically verified

We haven't yet run this listing's install command through our automated sandbox check. This isn't a red flag — we're steadily working through the catalog.

Manual Client & Custom JSON ConfigExpand JSON ▾

Client Config & Setup

Choose your client or environment

Target File:~/Library/Application Support/Claude/claude_desktop_config.json

claude_desktop_config.json

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

💡 Paste the JSON block into your client's configuration file under mcpServers, then restart the application.

Documentation Overview

mcp-z3-prover

MCP server exposing Z3 solver API

Install

Terminal

pip install mcp-z3-prover

Usage

server.ts

from mcp_z3_prover import mcp

# Run the server
mcp.run()

Or from command line:

bash

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

python

# 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

python

# 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

bash

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

Read the full README →View source on GitHub →

Related MCP Servers

View all in Developer Tools View all alternatives

Reviews

No reviews yet — be the first to share how this listing worked for you.

Frequently Asked Questions about MCP Z3 Prover

Add the following block to your claude_desktop_config.json under mcpServers: "mcpServers": { "mcp-z3-prover": { "command": "npx", "args": ["-y", "mcp-z3-prover"] } }

AllMCPs Directory Badge

Full Badge Customizer

Showcase your server listing on GitHub or your project documentation. Embed this dynamic SVG badge to highlight official listing status and live engagement.

Badge Style:

Live Dynamic SVG Preview

Markdown (GitHub README)

[![AllMCPs](https://allmcps.com/api/badge/mcp-z3-prover?style=directory)](https://allmcps.com/mcp/mcp-z3-prover)

HTML Embed

<a href="https://allmcps.com/mcp/mcp-z3-prover"><img src="https://allmcps.com/api/badge/mcp-z3-prover?style=directory" alt="MCP Z3 Prover on AllMCPs" /></a>

Technical Specs & Signals

CategoryDeveloper Tools

32Quality signal: Emerging · 32/100How this signal is calculated ▾

Server availabilityNot measured

Not scored for repo-hosted servers — we can't reach the running server, only its GitHub page. Hosted MCP endpoints are health-checked live.

Verified ownership10/20

Documentation & tools13/30

Adoption & activity1/15

Community engagement0/10

A guidance signal from public completeness & health data — not a user rating. New listings start lower and rise as they add docs, get verified, and grow adoption. Signals we can't observe for a listing are skipped, not counted against it.

★ Spotlight Slot

Feature Your MCP Server

Get maximum visibility for your server across our directory, search results, and detail pages.

Spotlight Your Server

Own this project?

This directory is pre-filled from public sources. Claim via GitHub README, site badge, or DNS TXT to unlock edit access and the Official badge and attach your website — proof is checked automatically, then reviewed by our team.

Free dofollow backlink: add your website and place the AllMCPs badge on it — no claim needed. We detect it automatically and keep it verified as long as the badge stays live.

Claim & get free dofollow

Share & Embed

Add our SVG badge (dark/light directory styles) or embeddable widget to your site.

Explore more

More in 💻 Developer Tools →Best MCP servers for Developers →Alternatives to MCP Z3 Prover →Install in Claude Desktop Install in Cursor Install in VS Code

Documentation Overview

mcp-z3-prover

MCP server exposing Z3 solver API

Install

Terminal

pip install mcp-z3-prover

Usage

server.ts

from mcp_z3_prover import mcp

# Run the server
mcp.run()

Or from command line:

bash

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

python

# 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

python

# 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

bash

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