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., "@Z3/SMT MCP Server solve x + y = 10, x - y = 4 for integers"
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 (Model Context Protocol) server that exposes Z3/SMT solver capabilities for constraint solving, logical reasoning, and satisfiability checking.
Direct Z3 Python code execution - Run arbitrary Z3 Python code
SMT-LIB 2.0 support - Parse and solve SMT-LIB format problems
Constraint checking - Check satisfiability of constraint lists
Theorem proving - Prove theorems by showing unsatisfiability of negation
Expression simplification - Simplify Z3 expressions
Logic program solving - Parse and solve structured logic programs (Logic-LLM format)
Session management - Incremental solving with push/pop support
Related MCP server: MCP Optimizer
# Using pip
pip install z3smt-mcp
# Or install from source
git clone https://github.com/z3smt-mcp/z3smt-mcp
cd z3smt-mcp
pip install -e .Python >= 3.10
z3-solver >= 4.12.0
mcp >= 1.0.0
# Run directly
z3smt-mcp
# Or via Python
python -m z3smt_mcp.serverAdd to your Claude Desktop config (claude_desktop_config.json):
{
"mcpServers": {
"z3smt": {
"command": "z3smt-mcp"
}
}
}Or if installed from source:
{
"mcpServers": {
"z3smt": {
"command": "python",
"args": ["-m", "z3smt_mcp.server"]
}
}
}solveExecute Z3 Python code directly. All Z3 imports are pre-loaded.
# Example: Solve a system of linear equations
x = Int('x')
y = Int('y')
solver = Solver()
solver.add(x + y == 10)
solver.add(x - y == 4)
if solver.check() == sat:
print(solver.model())
# Output: [y = 3, x = 7]solve_smtlibSolve problems in SMT-LIB 2.0 format.
(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
(assert (= (- x y) 4))
(check-sat)
(get-model)check_satCheck satisfiability of a list of constraints with automatic variable detection.
{
"constraints": ["x + y == 10", "x > 0", "y > 0", "x < y"]
}proveProve a theorem by showing its negation is unsatisfiable.
{
"theorem": "Implies(And(x > 0, y > 0), x + y > 0)",
"variables": {"x": "int", "y": "int"}
}simplifySimplify a Z3 expression.
{
"expression": "And(x > 0, Or(x > 0, y > 0))"
}solve_logic_programSolve structured logic programs in Logic-LLM format.
# Declarations
Color = EnumSort([red, green, blue])
assign = Function(Object -> Color)
# Constraints
assign(obj1) != assign(obj2)
Distinct([c:Color], assign(c))session_add_variable - Add a variable to the session
session_add_constraint - Add a constraint to the session
session_check - Check satisfiability and get model
session_push - Push a new context (for backtracking)
session_pop - Pop context (backtrack)
session_reset - Clear the session
list_sessions - List all active sessions
# Create a 9x9 grid of integer variables
X = [[Int(f"x_{i}_{j}") for j in range(9)] for i in range(9)]
solver = Solver()
# Each cell contains a value in 1-9
for i in range(9):
for j in range(9):
solver.add(And(X[i][j] >= 1, X[i][j] <= 9))
# Each row has distinct values
for i in range(9):
solver.add(Distinct(X[i]))
# Each column has distinct values
for j in range(9):
solver.add(Distinct([X[i][j] for i in range(9)]))
# Each 3x3 box has distinct values
for box_i in range(3):
for box_j in range(3):
box = [X[3*box_i + i][3*box_j + j]
for i in range(3) for j in range(3)]
solver.add(Distinct(box))
# Add known values (example)
solver.add(X[0][0] == 5)
solver.add(X[0][1] == 3)
# ... more constraints
if solver.check() == sat:
m = solver.model()
for i in range(9):
print([m[X[i][j]] for j in range(9)])# Solve for x where x * 3 == 21 in 8-bit arithmetic
x = BitVec('x', 8)
solver = Solver()
solver.add(x * 3 == 21)
if solver.check() == sat:
print(solver.model())# Find an array where a[0] + a[1] == 10
a = Array('a', IntSort(), IntSort())
solver = Solver()
solver.add(a[0] + a[1] == 10)
solver.add(a[0] > 0)
solver.add(a[1] > 0)
if solver.check() == sat:
print(solver.model())Z3 solver implementation adapted from Logic-LLM
MCP interface inspired by clingo-mcp
Z3 Theorem Prover by Microsoft Research
MIT License
Check satisfiability of a list of constraints.
Provide constraints as Z3 Python expressions. Variables will be auto-declared based on usage.
Example constraints:
"x + y == 10"
"x > 0"
"And(x < 100, y < 100)"
| Name | Required | Description | Default |
|---|---|---|---|
| constraints | Yes | List of Z3 constraint expressions | |
| variables | No | Variable declarations: {name: type} where type is 'int', 'real', 'bool', or 'bitvec:N' | |
| timeout_ms | No | Timeout in milliseconds (default: 30000) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries full burden. It mentions auto-declaration of variables but omits return format (sat/unsat/unknown), side effects, and required permissions. The timeout parameter default is in schema, not description.
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 description is concise, front-loaded with purpose, and uses a bullet list for examples. Every sentence adds value without redundancy.
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?
Despite having 3 parameters and no output schema, the description does not explain the return value of the tool or what 'checking' entails beyond constraints. The examples help but do not cover failure modes or expected output for unsatisfiability.
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 coverage is 100%, baseline 3. The description adds value by explaining constraints as Z3 expressions and that variables auto-declare based on usage, which goes beyond the schema's type descriptions. Examples further clarify usage.
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 clearly states 'Check satisfiability of a list of constraints' with a specific verb and resource. It distinguishes itself from sibling tools like 'prove' and 'solve' by being a direct check, and from session tools by being standalone.
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 implies usage for one-off constraint checking with auto-declared variables, but does not explicitly state when to use vs session-based siblings or provide exclusions. The example constraints give practical guidance.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
List all active solver sessions.
| Name | Required | Description | Default |
|---|---|---|---|
No parameters | |||
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description adds the behavioral context that this is a read-only listing of active sessions. However, it does not explain what 'active' means or how the list is returned.
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 description is a single, concise sentence that conveys the purpose without any redundant or unnecessary 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?
For a simple list tool with no parameters, the description is mostly complete. It could mention that no sessions exist or format, but it is adequate given sibling context.
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?
There are no parameters, and the schema has 100% coverage. The description does not need to add parameter info, so baseline of 4 applies.
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 clearly states the action (list) and the resource (active solver sessions), distinguishing it from sibling tools which perform operations like checking or pushing sessions.
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 implies this tool is used to retrieve a list of active sessions, but it does not explicitly state when to use it versus alternatives or mention any prerequisites.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Attempt to prove a theorem by showing its negation is unsatisfiable.
Provide the theorem as a Z3 expression. If the negation is unsatisfiable, the theorem is proven.
Example: prove "ForAll([x], x + 0 == x)" for integer x
| Name | Required | Description | Default |
|---|---|---|---|
| theorem | Yes | Z3 expression representing the theorem to prove | |
| variables | No | Variable declarations: {name: type} | |
| timeout_ms | No | Timeout in milliseconds (default: 30000) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description bears full responsibility for behavioral disclosure. It explains the logical process (proving by showing negation unsatisfiable) and mentions Z3. However, it does not specify side effects, authorization requirements, or what happens on success/failure. The absence of output schema exacerbates the gap, as return value behavior is unclear.
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 description is concise: three sentences and an example. It front-loads the purpose, then explains the method, and ends with a concrete example. Every sentence is purposeful with no redundant 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?
Given no output schema, the description should clarify what the tool returns. It only states the logical condition for proof ('If negation is unsatisfiable, the theorem is proven'), but does not specify the output format (e.g., boolean, proof object, or error). It also lacks information on error handling, timeout outcomes, or how variables are used. This is incomplete for an agent to properly invoke the tool.
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 coverage is 100%, so each parameter has a description in the schema. The tool description adds minimal value: it explains that the theorem is a Z3 expression and provides an example, but does not elaborate on the 'variables' parameter format or the timeout behavior beyond what is in the schema. The example omits variables, so no extra clarity is given for nested objects.
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 clearly states the tool's purpose: 'Attempt to prove a theorem by showing its negation is unsatisfiable.' It specifies the resource (a theorem) and the method (Z3 expression). The example reinforces usage, and it distinguishes itself from siblings like 'check_sat' (satisfiability check) and 'solve' (model finding).
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 explains when to use the tool (to prove a theorem) but does not explicitly state when not to use it or compare with alternatives. There is no guidance on when to choose this over siblings like 'check_sat' or 'solve', leaving the agent to infer context. The example is helpful but lacks exclusion criteria.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Add a constraint to the current solver session.
The constraint should be a valid Z3 expression using previously declared variables.
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | No | Session identifier (default: 'default') | default |
| constraint | Yes | Z3 constraint expression |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations provided; description mentions Z3 expression requirement and variable prerequisite but lacks details on side effects or error handling.
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?
Two concise sentences, no fluff, front-loaded with purpose.
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?
Adequate for a simple tool; could mention session existence requirement but overall sufficient given no output schema.
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 coverage is 100%, but description adds context that constraint must be a valid Z3 expression using previously declared variables, aiding interpretation.
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?
Description clearly states 'Add a constraint' to a solver session, distinguishing it from siblings like 'check_sat' and 'session_add_variable'.
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?
Implies prerequisite that variables must be declared using 'session_add_variable' first, but does not explicitly list alternatives or when to avoid.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Add a variable to the current solver session.
Supported types: int, real, bool, bitvec (with bits parameter)
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | No | Session identifier (default: 'default') | default |
| name | Yes | Variable name | |
| var_type | Yes | Variable type | |
| bits | No | Bit width for bitvec type (default: 32) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries full burden for behavioral disclosure. It mentions supported types and the bits parameter, but fails to disclose side effects (e.g., variable persistence, duplicate handling), error conditions (e.g., invalid session), or the fact that session_id defaults to 'default'. This is insufficient transparency.
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 description is two sentences, front-loaded with the primary action, and every word is necessary. There is no redundancy or verbose phrasing.
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?
Given the tool's role in a solver session and the presence of sibling tools like session_push/pop and session_add_constraint, the description lacks context about session lifecycle, variable uniqueness, or order of operations. No output schema is provided, so the description should at least hint at return values or state changes, which it does not.
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 coverage is 100%, so the baseline is 3. The description adds that bits is only relevant for bitvec, which is already implied by the schema. It does not provide additional meaning beyond what the schema offers, so no bonus.
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 clearly states the verb 'Add' and the resource 'variable to the current solver session', which distinguishes it from sibling tools like session_add_constraint that add constraints. The supported types are listed, providing a specific and immediately usable purpose.
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 implies that this tool is used to add variables to a session, but it does not provide explicit guidance on when to use it versus alternatives (e.g., before adding constraints) or any prerequisites (e.g., session must exist). No when-not-to-use scenarios are mentioned.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Check satisfiability of current session constraints and get the model if satisfiable.
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | No | Session identifier (default: 'default') | default |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations provided, so the description carries full burden. It does not disclose side effects, authorization needs, rate limits, or behavior when unsatisfiable (e.g., error vs. returning 'unsat').
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?
Single sentence, concise and to the point. No wasted words, but could be slightly more structured with separate statements for purpose and output.
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; description does not specify return format (e.g., model object, string). Given the complexity of satisfiability checking and sibling tools like 'solve' and 'check_sat', this is incomplete.
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 coverage is 100% with a well-described 'session_id' parameter. The description adds no meaning beyond the schema, so baseline 3 is appropriate.
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 clearly states the verb 'check', the resource 'session constraints', and the outcome 'get the model if satisfiable', distinguishing it from siblings like 'solve' or 'check_sat' that may operate without session context.
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?
No explicit guidance on when to use this tool versus alternatives like 'check_sat' or 'prove'. The phrase 'current session constraints' implies it is for session-based workflows, but exclusions and prerequisites are absent.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Pop a context from the solver stack (backtrack).
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | No | Session identifier (default: 'default') | default |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries full burden. It states 'pop' is destructive but fails to disclose edge cases (e.g., behavior when stack is empty) or any side effects. This is insufficient for a mutation 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 description is a single, efficient sentence with no redundant words. It is front-loaded and concise.
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?
Given the tool's simplicity (1 parameter, no output schema), the description is minimally adequate. However, it lacks details on error conditions or behavior when the stack is empty, which would improve completeness.
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 coverage is 100% with a single parameter (session_id) that has a clear description and default. The description adds no additional meaning beyond what the schema provides.
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 clearly states the verb 'pop' and the resource 'context from the solver stack' with the synonym 'backtrack'. It effectively distinguishes from siblings like session_push and session_reset.
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?
No explicit guidance on when to use this tool versus alternatives like session_reset. The context implies use after a push for backtracking, but no when-not-to-use or prerequisites are provided.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Push a new context onto the solver stack (for backtracking).
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | No | Session identifier (default: 'default') | default |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations, so description carries full burden. It only states the action without disclosing side effects like state mutation, memory consumption, or interaction with other tools. Minimal transparency.
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?
Single sentence, no wasted words. Efficiently conveys the core purpose.
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?
Given the simple nature of a push operation, the description is largely sufficient. However, it could mention return value or lack thereof, and that it modifies state. Still, it's adequate for a straightforward stack operation.
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 coverage is 100% with a clear description for 'session_id'. Description adds no extra meaning beyond the schema, so baseline score of 3 is appropriate.
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?
Description uses specific verb 'push' and resource 'context onto solver stack', clearly indicating the action. It distinguishes from sibling 'session_pop' by implying the opposite operation for backtracking.
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?
Implies usage when needing to create a backtracking point, but no explicit when-to-use, when-not-to-use, or alternatives provided. The context of 'for backtracking' hints at the purpose.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Reset the current solver session, clearing all variables and constraints.
| Name | Required | Description | Default |
|---|---|---|---|
| session_id | No | Session identifier (default: 'default') | default |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations provided, so the description bears the full burden. It clearly states the destructive nature ('clearing all variables and constraints'), which is adequate for a reset action.
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 description is a single, straightforward sentence with no wasted words.
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?
Given the tool's simplicity (1 optional parameter, no output schema), the description completely covers the necessary context.
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 coverage is 100% and the description adds no additional meaning beyond what the schema already provides for the session_id parameter.
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 uses a specific verb ('Reset') and resource ('solver session'), and clearly distinguishes from sibling tools like session_push/pop or session_add_constraint.
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 is implied that this tool is used to start a fresh session, but no explicit guidance on when to use vs alternatives (e.g., session_push/pop) or when not to use it.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Simplify a Z3 expression.
Returns the simplified form of the given expression.
Example: simplify "And(x > 0, x > 0)" -> "x > 0"
| Name | Required | Description | Default |
|---|---|---|---|
| expression | Yes | Z3 expression to simplify | |
| variables | No | Variable declarations: {name: type} |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations provided. The description indicates it returns the simplified form but does not disclose if it has side effects or requires certain conditions. Adequate for a simple read-only operation.
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?
Extremely concise with an effective example. Every sentence adds value, no wasted words.
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?
Given no output schema, the description adequately explains the return value. Could benefit from mentioning relationship to sibling tools like prove, but is sufficient for its purpose.
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 coverage is 100%, so parameters are well-defined. The description adds an example but no additional semantics beyond the schema.
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 clearly states the tool simplifies a Z3 expression and provides a concrete example, distinguishing it from sibling tools like prove and check_sat.
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?
No explicit guidance on when to use this tool versus alternatives, though the example implies it is for simplifying expressions before further analysis. Lacks comparative context.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Execute Z3 Python code to solve SMT constraints.
The code can use any Z3 Python API functions. Common imports (Solver, Int, Real, Bool, And, Or, Not, etc.) are pre-loaded.
Example:
x = Int('x')
y = Int('y')
solver = Solver()
solver.add(x + y == 10)
solver.add(x - y == 4)
if solver.check() == sat:
print(solver.model())| Name | Required | Description | Default |
|---|---|---|---|
| code | Yes | Z3 Python code to execute | |
| timeout_ms | No | Timeout in milliseconds (default: 30000) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, and the description fails to disclose key behaviors: return value (e.g., stdout), error handling, side effects (if any), or timeouts beyond the parameter. The example shows printing output, but the actual output format is unspecified.
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 description is concise with two paragraphs and an example, which is helpful. However, the example adds length; it could be more front-loaded with essential 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?
Without an output schema, the description should explain the return value and side effects. It does not, leaving the agent uncertain about what the tool actually produces or modifies. Error behavior and state changes are also 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?
Schema coverage is 100%, so the description adds minimal value beyond what the schema already provides. It mentions pre-loaded imports and gives an example, but does not clarify the code format or constraints.
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 clearly states that the tool executes Z3 Python code to solve SMT constraints, including an example. It distinguishes itself from siblings like check_sat and prove by being a general-purpose Z3 execution tool.
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 implies usage for arbitrary Z3 Python code but does not explicitly state when to use this tool versus alternatives like solve_logic_program or solve_smtlib.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Solve a structured logic program (Logic-LLM format).
The program should have sections:
EnumSort, IntSort, Function declarations
Logical constraints
Example:
# Declarations
Color = EnumSort([red, green, blue])
assign = Function(Object -> Color)
# Constraints
assign(obj1) != assign(obj2)| Name | Required | Description | Default |
|---|---|---|---|
| logic_program | Yes | Structured logic program | |
| timeout_ms | No | Timeout in milliseconds (default: 30000) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, and the description lacks information about side effects, error handling, or whether the solver modifies state. The timeout parameter is mentioned in schema but not in description.
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 description is reasonably concise, providing necessary format details and an example. It could be slightly more compact by trimming the example, but it remains focused.
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?
The description adequately covers the input format but fails to specify output behavior (e.g., returns solution or status). Given the complexity of the tool and lack of output schema, more guidance on expected results would improve completeness.
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 coverage is 100% with clear parameter descriptions. The description adds significant value by detailing the required format and providing a concrete example for the logic_program string parameter.
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 clearly states that the tool solves structured logic programs in Logic-LLM format, with an example distinguishing it from siblings like solve_smtlib that use SMT-LIB format.
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 explains the required sections and provides an example, but does not explicitly guide when to use this tool over alternatives like solve, prove, or check_sat.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Solve an SMT problem in SMT-LIB 2.0 format.
Example:
(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
(assert (= (- x y) 4))
(check-sat)
(get-model)| Name | Required | Description | Default |
|---|---|---|---|
| smtlib_code | Yes | SMT-LIB 2.0 format code | |
| timeout_ms | No | Timeout in milliseconds (default: 30000) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, and the description does not disclose behavioral traits such as handling of unsat results, timeout behavior, or output structure. The example only shows input, not output.
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 description is short and front-loaded with purpose. The example is helpful but could be trimmed to not repeat the obvious. It earns its place with minimal waste.
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?
The description lacks output schema or return value explanation. It does not clarify what the tool returns upon success or failure, leaving the agent without critical completion context.
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 100%, but the description adds no additional semantic meaning beyond the schema. It includes an example that implicitly demonstrates the 'smtlib_code' parameter but does not explain 'timeout_ms'.
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 clearly states 'Solve an SMT problem in SMT-LIB 2.0 format.' and provides a concrete example, making the purpose specific and distinct from sibling tools like 'solve' or 'check_sat'.
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?
There is no guidance on when to use this tool versus siblings like 'solve', 'prove', or 'check_sat'. No when-not-to-use or alternatives are mentioned.
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_satlist_sessionsprovesession_add_constraintsession_add_variablesession_checksession_popsession_pushsession_resetsimplifysolvesolve_logic_programsolve_smtlibScored across 13 tools
Most tools have clear distinct purposes, but check_sat, session_check, and solve all involve satisfiability checking and could cause confusion if descriptions are not carefully read. The session_* family is well-grouped.
Uses snake_case consistently, but some tools are single verbs (prove, simplify, solve) while others use noun_verb_noun pattern (session_add_constraint) or verb_noun (check_sat, list_sessions). The session_ prefix provides grouping but introduces inconsistency.
13 tools is appropriate for an SMT solver server, covering constraint solving, session management, multiple input formats, and theorem proving. Not too few or too many.
Covers core SMT operations well: standalone checking, session management, multiple input formats, and simplification. Minor gap: standalone check_sat may not return model, but session_check does. No explicit session deletion, but reset suffices.
Jailbreak-proof AI guardrails. Automated Reasoning SMT solver, not an LLM. ZK proofs included.
Deterministic reasoning stack for AI agents: simulate, decide & compute, plus cross-domain tools.
Precision math engine for AI agents. 203 exact methods. Zero hallucination.
Field operations on a deterministic solver — run jobs, crews & fleet from Claude or ChatGPT.
