jazz-z3-mcp

Z3 SMT solver exposed as MCP (Model Context Protocol) tools via a FastAPI HTTP server.

What it does

Provides a lightweight HTTP API wrapping the Z3 theorem prover, allowing LLM agents to perform formal constraint checking and satisfiability analysis.

Install

pip install jazz-z3-mcp
jazz-z3-mcp  # starts on port 8003

Docker

docker pull registry.gitlab.com/testmonkeyalpha/z3_mcp:latest
docker run -p 8003:8003 registry.gitlab.com/testmonkeyalpha/z3_mcp:latest

Health check

GET /health  →  {"status": "ok"}

---

Tools exposed

| Tool | Endpoint | Description | |------|----------|-------------| | z3_check | POST /tools/z3_check | Check satisfiability of constraints |

z3_check parameters

- variables: list of {name, type} where type is Int, Real, or Bool - constraints: list of Z3 expressions as Python-syntax strings (e.g. "x + y == 10", "x > 0")

Returns {sat: true, model: {...}} if satisfiable, or {sat: false} / {sat: false, error: "..."}.

---

Design: stateless solver

Every z3_check call is fully independent. There is no session concept — variables and constraints for a single check must all be sent together in one request. Nothing is stored server-side between calls.

---

Example usage

Basic satisfiability — integers

POST /tools/z3_check
{
  "variables": [{"name": "x", "type": "Int"}, {"name": "y", "type": "Int"}],
  "constraints": ["x + y == 10", "x > 0", "y > 0"]
}

{"sat": true, "model": {"x": "1", "y": "9"}}

Proving unsatisfiability

POST /tools/z3_check
{
  "variables": [{"name": "x", "type": "Int"}],
  "constraints": ["x > 5", "x < 3"]
}

{"sat": false}

Real-valued variables

POST /tools/z3_check
{
  "variables": [{"name": "r", "type": "Real"}],
  "constraints": ["r * r == 2", "r > 0"]
}

{"sat": true, "model": {"r": "1.41421356..."}}

Boolean reasoning

POST /tools/z3_check
{
  "variables": [{"name": "a", "type": "Bool"}, {"name": "b", "type": "Bool"}],
  "constraints": ["And(a, Not(b))", "Or(a, b)"]
}

{"sat": true, "model": {"a": "True", "b": "False"}}

---

Constraint syntax

Constraints are Python Z3 API expressions, not SMT-LIB2 syntax.

| Operation | Syntax | |-----------|--------| | Equality | x == 10 | | Inequality | x != y | | Arithmetic | x + y, x * z, x / y | | Logical AND | And(a, b) | | Logical OR | Or(a, b) | | Logical NOT | Not(a) | | Implication | Implies(a, b) | | If-then-else | If(cond, x, y) |

All Z3 Python API functions are available in constraint expressions.

---

Interpreting results

| Response | Meaning | |----------|---------| | {"sat": true, "model": {...}} | Satisfiable. Model assigns values that satisfy all constraints. | | {"sat": false} | Unsatisfiable. No assignment can satisfy all constraints simultaneously. | | {"sat": false, "error": "unknown ..."} | Solver returned unknown — happens with non-linear arithmetic or quantified formulas. Not the same as UNSAT. | | {"sat": false, "error": "Failed to parse constraint: ..."} | A constraint string could not be evaluated. |

Model values are always strings. Parse them as needed: - Int → int(model["x"]) - Real → may be a rational fraction like "1/3" — use fractions.Fraction(model["r"]) - Bool → model["a"] == "True"

---

Configuration

The server reads config.json at startup (path overridable via $CONFIG_PATH). All keys are optional; defaults are shown below.

{
  "solver_timeout_seconds": 10,
  "max_variables": 50,
  "max_constraints": 100
}

| Setting | Default | Notes | |---------|---------|-------| | solver_timeout_seconds | 10 | Max seconds Z3 may run per call before returning {"sat": "timeout"} | | max_variables | 50 | Requests with more variables are rejected with an error | | max_constraints | 100 | Requests with more constraints are rejected with an error | | Port | 8003 | Set via --port arg or $PORT env var | | Host | 0.0.0.0 | Binds all interfaces |

There is no authentication. Do not expose the service directly to public networks without an API gateway or proxy in front.

---

Known limitations

1. Stateless design. There is no session concept. All variables and constraints for a single check must be sent together in one z3_check request. Incremental solving across multiple calls is not supported.

2. Solver timeout. Long-running queries (e.g. quantifiers, non-linear arithmetic) are interrupted after solver_timeout_seconds and return {"sat": "timeout"}.

3. unknown is not an error. Z3 may return unknown for valid, well-formed queries it cannot decide. This is expected behavior for certain problem classes.

4. No authentication. All tool endpoints are unauthenticated.

5. Eval-based constraint parsing. Constraints are parsed via eval() against a restricted Z3 namespace. Malformed inputs produce Python exceptions caught and returned as structured errors.