Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@smt-mcp Does the conclusion 'q' follow from premises 'p' and 'p -> q'?"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
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.
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: Aare MCP
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"] }
}
}{
"mcpServers": {
"smt": { "type": "stdio", "command": "uv", "args": ["run", "--project", "/Users/ty/Projects/mine/smt-mcp", "smt-mcp"] }
}
}check_entailmentChecks 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_satisfiabilityChecks 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_smtlibRuns 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_infoReports 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 ..."}}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.
cd /Users/ty/Projects/mine/smt-mcp
uv run pytestCheck whether a conclusion is logically entailed by a set of premises, by asking whether (premises AND NOT conclusion) is unsatisfiable, cross-checked in both Z3 and cvc5.
YOU (the calling model) are responsible for translating the user's prose
question into declarations, premises, and conclusion. This server does
NOT interpret English — it only runs the SMT-LIB you hand it. Pass the
user's original wording in prose so the English and the formalization
travel together in the evidence trail.
Before presenting the verdict to the user as an answer about their original
English question, SHOW THEM THE FORMALIZATION (the declarations, premises,
and conclusion, or the assembled smtlib_script) and get their agreement
that it captures what they meant. A verdict from this tool is a fact about
the formalization, not directly about the user's English — whether the
formalization is a faithful translation of their intent is the user's call,
not yours.
Report exactly what the solvers returned. Do not upgrade "both solvers said
unsat under these bounds" into an unqualified "yes, this is true" — an
ENTAILMENT_HOLDS verdict is bounded-unsat relative to the premises and
declarations as written, not an unbounded proof about the world. Read the
caveats list and pass its contents along; each one names a specific way
the guarantee is weaker than it may sound (quantifiers, nonlinear
arithmetic, uninterpreted sorts, or a bounded check). If status comes back
DISAGREEMENT, that is the headline: tell the user the two solvers
returned different verdicts and that the result must not be trusted, do not
average or pick one to report.
declarations are full SMT-LIB forms, e.g. (declare-const x Int) or
(declare-fun key (String) String). premises and conclusion are bare
boolean terms, e.g. (> x 5) — this tool wraps each premise in (assert ...) for you (a premise that already starts with (assert is accepted
as-is, not double-wrapped).
Worked example (propositional modus ponens): declarations = ["(declare-const p Bool)", "(declare-const q Bool)"] premises = ["(=> p q)", "p"] conclusion = "q" -> entailment holds (both solvers report the negated-conclusion script is unsatisfiable).
| Name | Required | Description | Default |
|---|---|---|---|
| logic | No | ||
| prose | No | ||
| premises | Yes | ||
| conclusion | Yes | ||
| timeout_ms | No | ||
| declarations | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden and does so thoroughly: it discloses the dual-solver cross-check, the meaning of DISAGREEMENT, the caveats list, the bounded-unsat limitation, and the automatic (assert ...) wrapping of premises including the start-with-assert exception. This is unusually rich behavioral disclosure for a solver tool.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The purpose and mechanism are front-loaded in the first sentence, and the subsequent paragraphs on translation ownership, user confirmation, and verdict reporting each carry real decision-relevant content for a high-stakes tool. It is lengthy and could be tightened, but it is not padding.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
With six parameters, no annotations, and no output schema, the description does the heavy lifting: it names the meaningful return fields (status, caveats, ENTAILMENT_HOLDS, DISAGREEMENT) and defines the negation/unsat semantics. What is missing is a fuller picture of the response shape and the role of the `logic` parameter.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate, and it explains the format-critical parameters well: declarations are full SMT-LIB forms with examples, premises/conclusion are bare boolean terms (with wrapping behavior), and prose is the original wording carried in the evidence trail. It leaves `logic` (which SMT logic to select) and `timeout_ms` (only visible as a default) unexplained.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The first sentence states a precise verb+resource (check entailment of a conclusion by premises) and pins down the exact mechanism (unsatisfiability of premises AND NOT conclusion, cross-checked in Z3 and cvc5). That mechanism uniquely separates it from check_satisfiability and run_smtlib, so an agent can route without opening the schemas.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Strong contextual guidance: the calling model is told it owns the prose-to-SMT-LIB translation, must show the formalization to the user before presenting a verdict, and must treat DISAGREEMENT as untrusted. It does not, however, explicitly contrast when to reach for check_satisfiability or run_smtlib instead, so routing is implied rather than stated.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Check whether a set of constraints is jointly satisfiable, cross-checked in both Z3 and cvc5.
YOU (the calling model) are responsible for translating the user's prose
question into declarations and constraints. This server does NOT
interpret English — it only runs the SMT-LIB you hand it. Pass the user's
original wording in prose so the English and the formalization travel
together in the evidence trail.
Before presenting the verdict to the user as an answer about their original
English question, SHOW THEM THE FORMALIZATION (the declarations and
constraints, or the assembled smtlib_script) and get their agreement that
it captures what they meant. A verdict from this tool is a fact about the
formalization, not directly about the user's English.
Report exactly what the solvers returned. An UNSATISFIABLE verdict is
bounded-unsat relative to the constraints and declarations as written, not
an unbounded proof about the world — do not upgrade it into a stronger
claim. Read the caveats list and pass its contents along (quantifiers,
nonlinear arithmetic, uninterpreted sorts, or bounded checks each get their
own caveat). If status comes back DISAGREEMENT, that is the headline:
the two solvers returned different verdicts and the result must not be
trusted.
declarations are full SMT-LIB forms, e.g. (declare-const x Int).
constraints are bare boolean terms, e.g. (> x 5) — this tool wraps each
in (assert ...) for you (a constraint that already starts with (assert
is accepted as-is).
Example: declarations = ["(declare-const x Int)"] constraints = ["(> x 5)", "(< x 8)"] -> satisfiable (both solvers find a witness, e.g. x = 6).
| Name | Required | Description | Default |
|---|---|---|---|
| logic | No | ||
| prose | No | ||
| timeout_ms | No | ||
| constraints | Yes | ||
| declarations | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full behavioral burden and does so extensively. It discloses the cross-solver design, that the server does not interpret English, that UNSATISFIABLE is bounded relative to the formalization, that caveats must be surfaced, and that DISAGREEMENT is a headline untrustworthy result.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The definition is long but front-loaded with purpose and then organized into operational guidance. Most sentences carry useful constraints or warnings, though some procedural repetition could be tightened without losing meaning.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
No output schema exists, so the description must cover returns, and it does: verdicts, caveats, and DISAGREEMENT are all explained. It is nearly complete for a complex solver tool, with the main omission being parameter details for logic and timeout_ms.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate. It clearly explains declarations, constraints, and prose usage with an example, but it says nothing about the logic or timeout_ms parameters, leaving part of the five-parameter surface undocumented.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The first sentence names a specific operation and resource: checking joint satisfiability of constraints with cross-checking in Z3 and cvc5. That distinguishes it from a generic SMT runner, but no sibling tool is named, so an agent must infer the boundary with check_entailment or run_smtlib.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description gives clear procedural context: the caller must translate prose into declarations/constraints, show the formalization for user agreement, and report solver output exactly. However, it never says when to choose this tool over check_entailment or run_smtlib, so the when-vs-alternative guidance remains implicit.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Run a fully-assembled SMT-LIB v2 script verbatim, cross-checked in both Z3
and cvc5. Use this when check_entailment / check_satisfiability's fixed
shapes (declarations + premises/constraints + optional single conclusion)
are not expressive enough — e.g. you need multiple (check-sat) calls,
push/pop, or solver-specific tactics.
YOU (the calling model) build the entire script yourself, including
(check-sat). This server does not interpret English and does not modify
your script. As with the other tools: report exactly what came back, do not
upgrade unsat under bounds into an unbounded claim, and treat a
DISAGREEMENT between the two solvers as the headline finding, not a
footnote.
| Name | Required | Description | Default |
|---|---|---|---|
| script | Yes | ||
| timeout_ms | No |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations, so the description carries the full load, and it does substantial work: execution is verbatim, the server does not interpret English or modify the script, results are cross-checked across two solvers, solver DISAGREEMENT is the headline finding, and bounded unsat must not be upgraded. It leaves timeout/error behavior and the raw return shape unstated, keeping it short of a 5.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Front-loads what it does, then the usage trigger, then the caller responsibility and reporting discipline. Slightly verbose with multiple restated cautionary clauses, but every sentence carries distinct information.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
With no annotations and no output schema, the description covers the crucial epistemic guidance (report exactly what came back, don't overclaim unboundedness from bounded unsat). It does not describe return format or timeout semantics, but for a stateless script-runner this is close to sufficient.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0% over 2 params, so the description must compensate. It clarifies that `script` is the caller-authored full script including (check-sat), which adds real meaning, but `timeout_ms` is never explained (units, behavior on expiry) despite its 10000 default. Half the parameters remain semantically opaque.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific verb and resource ('Run a fully-assembled SMT-LIB v2 script verbatim, cross-checked in both Z3 and cvc5') and explicitly distinguishes itself from the sibling tools by naming their fixed shapes. An agent can tell it apart from check_entailment/check_satisfiability without opening a schema.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Gives an explicit when-to-use trigger: use this when check_entailment / check_satisfiability's fixed shapes (declarations + premises + single conclusion) are not expressive enough, with concrete examples (multiple check-sat, push/pop, solver-specific tactics). This is textbook alternative routing.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Report which Z3 and cvc5 binaries this server resolved (path, whether the binary was found, and its reported version string). Useful for confirming the environment before trusting any verdict from this server, and for attaching solver versions to an audit trail.
| Name | Required | Description | Default |
|---|---|---|---|
No parameters | |||
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full burden, and it does disclose the read-only reporting nature plus what happens if a binary is missing ('whether the binary was found'). It does not cover failure modes of the report itself or permissions, but for a zero-parameter diagnostic this is a solid disclosure.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single front-loaded sentence opening with the verb 'Report', then a compact parenthetical of returned fields and two brief justification clauses. Every clause earns its place with no padding.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
There is no output schema, but the description enumerates exactly what is returned (path, found status, version string) for both binaries, which fully compensates. Nothing an agent needs before calling a no-argument diagnostic tool is missing.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The tool takes no parameters, so the baseline is 4; there is nothing further the description could add on parameter meaning.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description states a specific verb and resource: it reports which Z3 and cvc5 binaries the server resolved, and enumerates the reporting fields (path, found flag, version string). It is clearly distinguishable in kind from the sibling check_entailment/check_satisfiability/run_smtlib tools, though it never names them or explicitly says it does not invoke a solver.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
It gives concrete usage contexts: confirming the environment before trusting any verdict, and attaching solver versions to an audit trail. That is clear when-to-use guidance, but there are no explicit alternatives or when-not-to-use conditions relative to the sibling solver-invoking tools.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
v0.1.0check_entailmentcheck_satisfiabilityrun_smtlibsolver_infoScored across 4 tools
Each tool has a clearly distinct role: check_entailment tests logical consequence, check_satisfiability tests joint consistency, run_smtlib is an explicit escape hatch for arbitrary scripts, and solver_info reports environment info. The descriptions even explain when to prefer run_smtlib over the fixed-shape tools, eliminating the main potential overlap.
check_entailment, check_satisfiability, and run_smtlib follow a consistent verb_noun pattern, and solver_info is a readable noun form. The one deviation (solver_info lacking a verb) is minor and idiomatic.
Four tools is well-scoped for a focused SMT solver wrapper: two fixed-shape query forms, one general script runner, and one environment-inspection tool. Each earns its place with no redundancy or thin coverage.
The surface covers the core SMT workflow (entailment, satisfiability, raw scripts, solver version info). Minor gaps exist for dedicated model/witness retrieval and unsat-core or optimization queries, though run_smtlib can partially work around these.
Jailbreak-proof AI guardrails. Automated Reasoning SMT solver, not an LLM. ZK proofs included.
Check claims against a fact-store: consistent, contradicts, or unverifiable — with a receipt.
MCP-native AI evaluation: rubric audits, eval suites, and proof reports for AI/LLM output.
Zero-trust logic judge: your AI writes a claim as a ZFL table, the ZTL core judges it.
