# 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.

## 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.

```bash
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:

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

### Local dev variant

```json
{
  "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.

```python
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.

```python
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.

```python
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.

```python
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

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