Claude MarketplacesSubmit

Mcp Z3 Prover

daedalus/mcp-z3-prover

Wraps the Z3 theorem prover so you can solve constraint satisfaction and optimization problems through MCP tools. Create Boolean, integer, and real variables, add constraints in a straightforward string syntax, then call solve or optimize to get satisfying assignments. The factorization example shows the flavor: define two integer variables p and q, constrain their product to equal a target number, add bounds and parity checks, and let Z3 find the factors. Useful when you need symbolic math solving, SMT queries, or constraint-based search without writing Python scripts directly. Each solver session maintains state across calls until you reset it.

tools: 11
transport: STDIO
last updated: Mar 28, 2026

Tools

11 tools

Public tool metadata for what this MCP can expose to an agent.

create_bool_varCreate a Boolean variable

Create a Boolean variable

No parameter schema in public metadata yet.

create_int_varCreate an Integer variable

Create an Integer variable

No parameter schema in public metadata yet.

create_real_varCreate a Real variable

Create a Real variable

No parameter schema in public metadata yet.

create_int_constantCreate an integer constant

Create an integer constant

No parameter schema in public metadata yet.

create_real_constantCreate a real constant

Create a real constant

No parameter schema in public metadata yet.

add_constraintAdd a constraint to the solver

Add a constraint to the solver

No parameter schema in public metadata yet.

solveSolve the current problem

Solve the current problem

No parameter schema in public metadata yet.

get_model_valueGet value of a variable from the model

Get value of a variable from the model

No parameter schema in public metadata yet.

optimizeSolve with optimization objective

Solve with optimization objective

No parameter schema in public metadata yet.

reset_solverReset the solver state

Reset the solver state

No parameter schema in public metadata yet.

list_variablesList all created variables

List all created variables

No parameter schema in public metadata yet.

Sponsors

Promote your product hereReach 125k+ visitors monthly Promote your product hereReach 125k+ visitors monthly

Agent CaffeineSponsoredClose your lid, come back to finished work

SnugSponsoredThe clipboard manager for the AI era Promote your product hereReach 125k+ visitors monthly

WaxSponsoredBlock anything with supervision, without erasing your iPhone Promote your product hereReach 125k+ visitors monthly

knobsSponsoredSee your site on any phone, any day, in any language

Readme

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:

View the full README on GitHub

Details

Repository: github.com/daedalus/mcp-z3-prover
Package: mcp-z3-prover
Transport: STDIO
Registry: MCP registry, active