How do I install io.github.daedalus/mcp-z3-prover?

Clone io.github.daedalus/mcp-z3-prover from https://github.com/daedalus/mcp-z3-prover and configure it as an MCP server in your client (Claude Desktop, Cursor, or VS Code).

Is io.github.daedalus/mcp-z3-prover open source?

Yes, io.github.daedalus/mcp-z3-prover is open source under the MIT license. Source code is available at https://github.com/daedalus/mcp-z3-prover.

What category does io.github.daedalus/mcp-z3-prover belong to?

io.github.daedalus/mcp-z3-prover is listed under Developer Tools MCP servers on MCPFind.

io.github.daedalus/mcp-z3-prover — MCP Server for Developer Tools

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

Set up in your AI client

AI clientOperating system

Merge this template into ~/Library/Application Support/Claude/claude_desktop_config.json. Keep existing servers. Add any arguments, credentials, and permissions required by the maintainer; this template has not been install-tested.

json

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

Restart Claude Desktop completely for changes to take effect. Confirm the server appears connected in the client’s tool list, then try a read-only example from its documentation.

Claude Desktop setup reference

Compatible MCP Clients

io.github.daedalus/mcp-z3-prover works with any MCP-compatible client. Copy the config snippet from the Configuration section above and add it to the file shown for your client, then restart the application.

Claude Desktop~/Library/Application Support/Claude/claude_desktop_config.jsonRestart Claude Desktop completely for changes to take effect.

Cursor~/.cursor/mcp.jsonRestart Cursor for changes to take effect.

VS Code.vscode/mcp.jsonReload VS Code window for changes to take effect.

Windsurf~/.codeium/windsurf/mcp_config.jsonRestart Windsurf for changes to take effect.

Claude Code.mcp.jsonSave at the project root, then start Claude Code in that project and review the MCP server approval prompt. Keep real credentials out of shared files.

io.github.daedalus/mcp-z3-prover