Mcp Z3 Prover

io.github.daedalusPublished by GitHub account daedalusv0.1.0Updated Oct 28, 2026

MCP server exposing Z3 solver API

VerifiedSTDIODesktop onlyDeveloper ToolsAI & ML

Overview

AI-generated overview

Local MCP server that exposes the Z3 solver so an assistant can build variables and constraints, then solve or optimize them.

What you can do
  • Create Boolean, integer and real variables and integer or real constants
  • Add constraints to the solver and solve the current problem
  • Read variable values from the resulting model
  • Solve with an optimization objective
  • Reset the solver state and list all created variables
When to use it
Useful when you want an assistant to check whether a set of logical or arithmetic constraints is satisfiable, find a satisfying assignment, or optimize an objective, such as small factoring or puzzle-style problems.
Requirements
Runs as a local process installed from the PyPI package mcp-z3-prover (pip install mcp-z3-prover) and started with the mcp-z3-prover command; desktop only. No authentication, environment variables or headers are declared.
Before you install
The solver keeps state between calls, so constraints accumulate until the solver is reset; expect long runtimes or heavy CPU use on hard problems. No credentials, payments or third-party data sharing are indicated.

Installation

In SourceWeft

  1. Open Mcp Z3 Prover in the dashboard and add it to a workspace.
  2. Enable the server for the chats that should use its tools.

Desktop only via STDIO. STDIO servers start a local process, so they need the SourceWeft desktop host.

Other MCP clients

Follow the launch instructions in the repository.

README

mcp-z3-prover

MCP server exposing Z3 solver API

[PyPI] [Python] [Ruff]

Install

bash
pip install mcp-z3-prover

Usage

python
from mcp_z3_prover import mcp
# Run the servermcp.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 variablescreate_int_var("x")create_int_var("y")
# Add constraintsadd_constraint("int:x + int:y == 10")add_constraint("int:x > 0")add_constraint("int:y > 0")
# Solveresult = solve()# Returns: {"status": "sat", "model": {"x": "5", "y": "5"}}
# Get specific valuesx_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 constraintsadd_constraint("int:p * int:q == 4295229443")add_constraint("4295229443 > int:p")add_constraint("4295229443 > int:q")add_constraint("int:q <= 65537")  # sqrt(4295229443) ≈ 65537add_constraint("int:q > 1")add_constraint("int:p > 1")add_constraint("int:q % 2 != 0")  # q is oddadd_constraint("int:p % 2 != 0")  # p is odd
# Solveresult = solve()# Returns: {"status": "sat", "model": {"p": "65539", "q": "65537"}}# Verification: 65537 * 65539 = 4295229443

Development

bash
git clone https://github.com/daedalus/mcp-z3-prover.gitcd mcp-z3-proverpip install -e ".[test]"
# run testspytest
# formatruff format src/ tests/
# lintruff check src/ tests/
# type checkmypy src/

MCP Registration

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

Source: README.md at commit 12bcd34

Tools

0
SourceWeft has not started this package in its sandbox yet, so its tools are not known.

Version history

1
  1. v0.1.0LatestSep 16, 2026

Score

50% of the applicable checks met

How complete this listing is, computed from the registry entry, the endpoint and public sources. Not a rating of the server and not a statement that it is safe or working today: reachability is a dated check, and no installs or reviews go into the score.

  • Reached in the last 30 days25 pts

    Keep the endpoint answering the MCP handshake; SourceWeft probes it every 30 days.

  • Auth declared10 pts

    Declare the credential headers in the registry entry, or keep the endpoint answering the probe so its auth can be classified.

  • Tools listed15 pts

    Answer tools/list without a credential, or ship a package that starts in a sandbox without one.

  • DescriptionRequired15 pts
  • Logo10 pts
  • Documentation15 pts
  • License10 pts