smt-mcp

An MCP server that answers logical entailment and satisfiability questions by dispatching to SMT solvers (Z3 and cvc5), and returns auditable evidence rather than a bare yes/no.

There is no LLM inside this server. The calling model — the MCP client, e.g. Claude — is responsible for translating a user's prose question into an SMT-LIB formalization (declarations, premises/constraints, a conclusion). This server takes that formalization, runs it through both solvers deterministically, and reports exactly what came back: which verdict each solver returned, the raw output, a counterexample or witness model when one exists, and a list of caveats about what the result does and does not prove.

Why cross-checking two solvers matters

A single SMT solver's unsat is a single point of failure for a proof claim: a bug in the solver, or a subtle mismatch between what you meant and what you wrote, can produce a confident wrong answer. Every check in this server runs in both Z3 and cvc5, independently. If they agree, that is real corroboration. If they disagree, that disagreement is reported as the headline finding (status: "DISAGREEMENT") — never averaged, never silently resolved by picking one. And unknown (a timeout, an incomplete decision procedure, a solver error) is never coerced into unsat or sat: entailment is only reported as holding when both solvers say so.

Related MCP server: Logic-LM MCP Server

Install

Requires Z3 and cvc5 installed locally (on macOS: brew install z3 cvc5). Binaries are resolved via shutil.which, falling back to /opt/homebrew/bin/z3 and /opt/homebrew/bin/cvc5, and can be overridden with the SMT_MCP_Z3 / SMT_MCP_CVC5 environment variables.

cd /Users/ty/Projects/mine/smt-mcp
uv venv
uv pip install -e ".[dev]"

~/.claude.json (or any MCP-client config)

Run directly from the project directory with uvx, no separate install step:

{
  "mcpServers": {
    "smt": { "type": "stdio", "command": "uvx", "args": ["--from", "/Users/ty/Projects/mine/smt-mcp", "smt-mcp"] }
  }
}

Local dev variant

{
  "mcpServers": {
    "smt": { "type": "stdio", "command": "uv", "args": ["run", "--project", "/Users/ty/Projects/mine/smt-mcp", "smt-mcp"] }
  }
}

Tools

check_entailment

Checks whether a conclusion follows from a set of premises, by asking whether premises AND NOT conclusion is unsatisfiable — cross-checked in both solvers.

check_entailment(
    declarations=["(declare-const p Bool)", "(declare-const q Bool)"],
    premises=["(=> p q)", "p"],
    conclusion="q",
)
# -> status: "ENTAILMENT_HOLDS" (both solvers proved the negated-conclusion
#    script unsatisfiable)

check_satisfiability

Checks whether a set of constraints is jointly satisfiable.

check_satisfiability(
    declarations=["(declare-const x Int)"],
    constraints=["(> x 5)", "(< x 8)"],
)
# -> status: "SATISFIABLE", witness mentions x (e.g. x = 6)

run_smtlib

Runs a fully-assembled SMT-LIB v2 script verbatim (your own (check-sat), push/pop, multiple queries, solver-specific tactics), cross-checked the same way.

run_smtlib("(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n(get-model)")
# -> status: "SAT"

solver_info

Reports which Z3 and cvc5 binaries were resolved, their paths, and their version strings — useful for attaching solver versions to an audit trail before trusting any verdict.

solver_info()
# -> {"z3": {"path": "...", "found": true, "version": "Z3 version 4.16.0 ..."},
#     "cvc5": {"path": "...", "found": true, "version": "cvc5 1.3.4 ..."}}

What this does not prove

A verdict from this server is a fact about the formalization and the bounds as written — not directly about the user's original English, and not about the world.

• The formalization might not capture the intent. The calling model writes the declarations/premises/conclusion; whether that translation is faithful to what the user meant is the user's judgment call, not the solver's. Show the formalization (or the assembled smtlib_script) before presenting a verdict as an answer to the user's actual question.

• unsat under bounds is bounded-unsat, not an unbounded proof. If the script only asserts x > 5 and x < 100, an unsat result says nothing about x outside that range. The caveats field flags this whenever a bound literal is detected.

• Quantifiers, nonlinear arithmetic, and uninterpreted sorts weaken the guarantee further — each gets its own caveat when detected, because unknown becomes a live possibility and an unsat over an uninterpreted function is a statement about all interpretations, not a concrete counterexample search.

• A DISAGREEMENT between the two solvers means don't trust either verdict until the discrepancy is understood — it is surfaced as the top-level status precisely so it cannot be missed.

Running the tests

cd /Users/ty/Projects/mine/smt-mcp
uv run pytest