Z3/SMT MCP Server

Server Quality Checklist

Profile completionA complete profile improves this server's visibility in search results.

Latest release: v0.1.0
Disambiguation4/5
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.
Naming Consistency4/5
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.
Tool Count5/5
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.
Completeness4/5
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.
Average 3.6/5 across 13 of 13 tools scored. Lowest: 2.9/5.
See the Tool Scores section below for per-tool breakdowns.
- No community issues in the last 6 months
- 0 commits in the last 12 weeks
- Last stable release on January 24, 2026
- No critical vulnerability alerts
- No high-severity vulnerability alerts
- No code scanning findings
- CI is passing
This repository is licensed under MIT License.
This repository includes a README.md file.
No tool usage detected in the last 30 days. Usage tracking helps demonstrate server value.
Tip: use the "Try in Browser" feature on the server page to seed initial usage.
Add a glama.json file to provide metadata about your server.
If you are the author, simply .
If the server belongs to an organization, first add glama.json to the root of your repository:
```
{
  "$schema": "https://glama.ai/mcp/schemas/server.json",
  "maintainers": [
    "your-github-username"
  ]
}
```
Then . Browse examples.
Add related servers to improve discoverability.

How to sync the server with GitHub?

Servers are automatically synced at least once per day, but you can also sync manually at any time to instantly update the server profile.

To manually sync the server, click the "Sync Server" button in the MCP server admin interface.

How is the quality score calculated?

The overall quality score combines two components: Tool Definition Quality (70%) and Server Coherence (30%).

Tool Definition Quality measures how well each tool describes itself to AI agents. Every tool is scored 1–5 across six dimensions: Purpose Clarity (25%), Usage Guidelines (20%), Behavioral Transparency (20%), Parameter Semantics (15%), Conciseness & Structure (10%), and Contextual Completeness (10%). The server-level definition quality score is calculated as 60% mean TDQS + 40% minimum TDQS, so a single poorly described tool pulls the score down.

Server Coherence evaluates how well the tools work together as a set, scoring four dimensions equally: Disambiguation (can agents tell tools apart?), Naming Consistency, Tool Count Appropriateness, and Completeness (are there gaps in the tool surface?).

Tiers are derived from the overall score: A (≥3.5), B (≥3.0), C (≥2.0), D (≥1.0), F (<1.0). B and above is considered passing.

Tool Scores

Behavior2/5
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.
Conciseness4/5
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.
Completeness2/5
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.
Parameters2/5
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.
Purpose5/5
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.
Usage Guidelines2/5
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.
Behavior2/5
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.
Conciseness4/5
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.
Completeness2/5
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.
Parameters3/5
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.
Purpose5/5
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.
Usage Guidelines3/5
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.
Behavior2/5
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.
Conciseness5/5
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.
Completeness3/5
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.
Parameters3/5
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.
Purpose5/5
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.
Usage Guidelines2/5
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.
Behavior2/5
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.
Conciseness4/5
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.
Completeness2/5
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.
Parameters3/5
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.
Purpose5/5
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.
Usage Guidelines3/5
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.
Behavior2/5
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.
Conciseness5/5
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.
Completeness2/5
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.
Parameters3/5
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.
Purpose5/5
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.
Usage Guidelines3/5
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.
Behavior3/5
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.
Conciseness5/5
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.
Completeness2/5
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.
Parameters3/5
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.
Purpose5/5
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.
Usage Guidelines3/5
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.
Behavior2/5
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.
Conciseness5/5
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.
Completeness4/5
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.
Parameters3/5
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.
Purpose5/5
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.
Usage Guidelines3/5
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.
Behavior2/5
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.
Conciseness4/5
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.
Completeness3/5
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.
Parameters4/5
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.
Purpose5/5
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.
Usage Guidelines3/5
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.
Behavior2/5
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.
Conciseness5/5
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.
Completeness2/5
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.
Parameters4/5
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.
Purpose5/5
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.
Usage Guidelines4/5
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.
Behavior3/5
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.
Conciseness5/5
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.
Completeness4/5
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.
Parameters3/5
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.
Purpose5/5
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.
Usage Guidelines3/5
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.
Behavior3/5
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.
Conciseness5/5
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.
Completeness4/5
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.
Parameters4/5
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.
Purpose5/5
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.
Usage Guidelines3/5
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.
Behavior4/5
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.
Conciseness5/5
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.
Completeness5/5
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.
Parameters3/5
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.
Purpose5/5
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.
Usage Guidelines3/5
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.
Behavior3/5
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.
Conciseness5/5
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.
Completeness4/5
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.
Parameters4/5
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.
Purpose5/5
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.
Usage Guidelines4/5
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.

GitHub Badge

Glama performs regular codebase and documentation scans to:

Confirm that the MCP server is working as expected.
Confirm that there are no obvious security issues.
Evaluate tool definition quality.

Our badge communicates server capabilities, safety, and installation instructions.

Card Badge

Copy to your README.md:

[![z3smt-mcp MCP server](https://glama.ai/mcp/servers/NewJerseyStyle/z3smt-mcp/badges/card.svg)](https://glama.ai/mcp/servers/NewJerseyStyle/z3smt-mcp)

Score Badge

Copy to your README.md:

[![z3smt-mcp MCP server](https://glama.ai/mcp/servers/NewJerseyStyle/z3smt-mcp/badges/score.svg)](https://glama.ai/mcp/servers/NewJerseyStyle/z3smt-mcp)

Latest Blog Posts

Who's Calling? MCP Hosts Are an Identity Blind Spot (And the Spec Knows It)
By Om-Shree-0709 on July 25, 2026.
mcp
Agent Identity
OAuth 2.1
Your AI Chatbot Just Exposed Your CEO's Salary to an Intern
By Om-Shree-0709 on July 2, 2026.
Agent Identity
MCP Security
OAuth Delegation
Why MCP Servers Need Execution Sandboxing (And Why Your Current Stack Isn't Enough)
By Om-Shree-0709 on June 30, 2026.
Agentic Ai
Prompt Injection
WebAssembly

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/NewJerseyStyle/z3smt-mcp'

If you have feedback or need assistance with the MCP directory API, please join our Discord server