MCP.Market

Z3 Prover MCP server

by daedalus·io.github.daedalus/mcp-z3-prover·v0.1.0·1 stars
No reviews yet

MCP server exposing Z3 solver API

B74/100grade B
Write a reviewInstall
What users say
No reviews yet
Be the first
Safety scan
B74/100

full report

Adoption
New

1 stars12 downloads/wk

Reviews

Write one

Nobody has reviewed Z3 Prover yet.

If you have run it, two minutes of your experience saves the next person an afternoon.

Z3 Prover tools (11, 5 write)

write = sends, deletes, buys or posts

Read from the package source without running it. The installed server may list more.

  • add_constraint

    Add a constraint to the solver. Use variable references like 'bool:x', 'int:y', 'real:z' in expressions.

  • create_bool_varwrite action

    Create a Boolean variable with the given name.

  • create_int_constantwrite action

    Create an integer constant with the given value.

  • create_int_varwrite action

    Create an Integer variable with the given name.

  • create_real_constantwrite action

    Create a real constant with the given value.

  • create_real_varwrite action

    Create a Real variable with the given name.

  • get_model_value

    Get the value of a variable from the model after solving.

  • list_variables

    List all created variables.

  • optimize

    Solve with optimization objective (maximize or minimize).

  • reset_solver

    Reset the solver state (clear all variables, constraints, and model).

  • solve

    Solve the current problem and return the result.

Public scan report

scanner v0.1.9 · 2026-09-27 · same rubric, same numbers if you re-run it

1 medium
  • Code scan4 source files scanned20/25
  • –Live reliabilityno gateway calls yet and no remote to proben/a
  • –Tool poisoningtools not inspected (local package is not executed); not countedn/a
  • Auth qualitylocal package, no credentials required12/15
  • Maintenancelast push 158 days ago8/15
  • Maintainer identityregistry namespace matches repository owner; GitHub account older than a year8/10

Findings (1)

  • mediumeval / new Function usedexec.eval
    mcp_z3_prover-0.1.0/src/mcp_z3_prover/_core.py: …t_map": session.constants} result = eval(expr, {"__builtins__": {}}, local_vars) …
Overall 74/100. Components that don't apply are left out of the denominator. Any critical finding is an F.RubricAppeal a findingJSON

How Z3 Prover compares

Against every graded MCP server, from our own scans and uptime checks. Updated after each scan run.

Safety score
74/100
higher than 43% of 48,273 servers
Tools
11
the typical server has 7
Tools that change things
45%
typical: 0%. Fewer write tools means less an agent can break
GitHub stars
1
more than 65% of 28,534 servers
Downloads a week
12
more than 3% of 11,915 servers with a package

What its tools let an agent do: 5 read · 6 create

Install Z3 Prover in Claude Code, Cursor or VS Code

claude mcp add mcp-z3-prover -- uvx mcp-z3-prover
Add to Cursor

What the publisher says

From the Z3 Prover repository's README, as published. We do not edit it. Read it on GitHub

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:

  • createboolvar - Create a Boolean variable
  • createintvar - Create an Integer variable
  • createrealvar - Create a Real variable
  • createintconstant - Create an integer constant
  • createrealconstant - Create a real constant
  • addconstraint** - Add a constraint to the solver
  • solve - Solve the current problem
  • getmodelvalue - Get value of a variable from the model
  • optimize - Solve with optimization objective
  • resetsolver** - Reset the solver state
  • listvariables** - 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

Nothing above is checked by us. What we check is on the safety report.

Z3 Prover: common questions

Is Z3 Prover MCP server safe?
Mostly: it is graded B (74/100). Read the Z3 Prover safety report
How do I install Z3 Prover?
It runs on your machine. Copy the Claude Code, Cursor, VS Code or Claude Desktop config from the install section.
Does Z3 Prover need an API key?
Not as far as the registry entry and our scan can tell: no credentials are declared or required.
Is Z3 Prover maintained?
The last commit was 194 days ago (2026-04-22). The latest release is v0.1.0.
How does Z3 Prover compare with other MCP servers?
safety score 74/100 (higher than 43% of 48,273 servers); tools 11 (the typical server has 7); tools that change things 45% (typical: 0%. Fewer write tools means less an agent can break). Full comparison.

More from daedalus →