About
MCP server exposing Z3 solver API
Security Report
Valid MCP server (3 strong, 4 medium validity signals). 1 code issue detected. 5 known CVEs in dependencies (1 critical, 3 high severity) Package registry verified. Imported from the Official MCP Registry.
8 files analyzed · 7 issues found
Security scores are indicators to help you make informed decisions, not guarantees. Always review permissions before connecting any MCP server.
How to Install
Add this to your MCP configuration file:
{
"mcpServers": {
"io-github-daedalus-mcp-z3-prover": {
"args": [
"mcp-z3-prover"
],
"command": "uvx"
}
}
}Documentation
View on GitHubFrom the project's GitHub 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:
- 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
Reviews
No reviews yet
Be the first to review this server!
More Developer Tools MCP Servers
Git
Freeby Modelcontextprotocol · Developer Tools
Read, search, and manipulate Git repositories programmatically
Fetch
Freeby Modelcontextprotocol · Developer Tools
Web content fetching and conversion for efficient LLM usage
Toleno
Freeby Toleno · Developer Tools
Toleno Network MCP Server — Manage your Toleno mining account with Claude AI using natural language.
mcp-creator-python
Freeby mcp-marketplace · Developer Tools
Create, build, and publish Python MCP servers to PyPI — conversationally.
MCP Marketplace
Freeby mcp-marketplace · Developer Tools
Search and install MCP servers from inside your AI client.
MarkItDown
Freeby Microsoft · Content & Media
Convert files (PDF, Word, Excel, images, audio) to Markdown for LLM consumption