mcpField
M
mcp-z3-prover

mcp-z3-prover

Local
github.com/daedalusScience & Education1Updated 27w ago
Repository

About mcp-z3-prover

mcp-z3-prover exposes the Z3 solver API as an MCP server. It supports clients that build constraint problems, solve or optimize them, and inspect variable values.

Key features

  1. 01Create Boolean, integer, and real variables
  2. 02Add solver constraints
  3. 03Solve constraint problems
  4. 04Optimize an objective
  5. 05Read model values and list variables
  6. 06Reset solver state

Use cases

  1. 01Model a problem with variables and constraints
  2. 02Find solutions to integer or real constraints
  3. 03Optimize a solver objective
  4. 04Inspect solution values or restart the solver

MCP support

Exposes Z3 solver tools to MCP clients for variable creation, constraint management, solving, optimization, model inspection, and reset.

Configuration

Local server config is the same for every client. Copy it into your client’s MCP config file.

mcp.json · Universal config
{
  "mcpServers": {
    "daedalus-mcp-z3-prover": {
      "command": "uvx",
      "args": [
        "mcp-z3-prover"
      ]
    }
  }
}
Run commanduvx mcp-z3-prover

Local servers need a runtime on your machine (e.g. Node.js 18+). Config file locations differ by client; see your client’s docs.

Packages
pypimcp-z3-prover0.1.0

Tools

11

Saved tool list · updated 2w ago

ParameterTypeRequiredDescription
namestringYes

Details

From the project README

mcp-z3-prover

MCP server exposing Z3 solver API

PyPI Python Ruff

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

Comments

Markdown supported

New to MCP?

From what the protocol is to installing your first server, these answers cover most first questions.

An open protocol that defines how AI applications connect to external tools and data in a uniform way. Clients talk to the model; MCP servers provide tools, resources and prompt templates. They exchange standard messages, so one server can be reused by many clients.