Skip to main content
Glama
dsouflis

z3-solver-mcp-server

by dsouflis
OverviewSchemaRelated ServersScoreDiscussions
Python
Local

Z3 SMT Solver MCP Server

A Model Context Protocol (MCP) server that provides SMT (Satisfiability Modulo Theories) solving capabilities using the Z3 theorem prover. This server allows Claude and other MCP clients to solve complex constraint satisfaction problems, mathematical equations, logic puzzles, and optimization problems.

Features

  • SMT-LIB2 Support: Accepts problems in the standard SMT-LIB2 format

  • Z3 Integration: Powered by Microsoft's Z3 theorem prover

  • Mathematical Problem Solving: Handle algebra, logic, optimization, and constraint satisfaction

  • Simple Interface: Single tool with string input/output

Related MCP server: Logic-LM MCP Server

Installation

Prerequisites

  • Python 3.8 or higher

  • uv (recommended) or pip

Setup

  1. Clone this repository:

git clone <repository-url>
cd z3-mcp-server

  1. Install dependencies:

uv sync

Or with pip:

pip install z3-solver mcp

  1. Make the server executable:

chmod +x src/z3_mcp_server/main.py

Usage

With Claude Desktop

Add the server to your Claude Desktop configuration file:

macOS: ~/Library/Application Support/Claude/claude_desktop_config.json Windows: %APPDATA%/Claude/claude_desktop_config.json

{
  "mcpServers": {
    "z3-solver": {
      "command": "uv",
      "args": ["--directory", "/path/to/z3-mcp-server", "run", "main.py"],
      "env": {}
    }
  }
}

Example Problems

Once configured, you can ask Claude to solve various types of problems:

Age Problems:

"Joey is 20 years younger than Becky. In two years, Becky will be twice as old as Joey. How old are they?"

Algebra:

"Find integers x and y such that 2x + 3y = 17 and both are positive."

Logic Puzzles:

"Three people have ages 21, 22, and 23. Alice is not 21, and Bob is older than Alice. What are their ages?"

Optimization:

"A farmer has 100 feet of fencing. What rectangular dimensions maximize the enclosed area?"

Tool Reference

solve_smt_lib2

Solves constraint problems specified in SMT-LIB2 format.

Parameters:

  • problem (string): The constraint problem in SMT-LIB2 syntax

Returns:

  • String containing the solver result:

    • sat + model if satisfiable

    • unsat if no solution exists

    • unknown if solver cannot determine

    • Error message if parsing fails

Example SMT-LIB2 Input:

(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
(assert (= (* x y) 21))
(check-sat)
(get-model)

SMT-LIB2 Quick Reference

Basic Syntax

  • (declare-const name Type) - Declare a variable

  • (assert condition) - Add a constraint

  • (check-sat) - Check if constraints are satisfiable

  • (get-model) - Get variable assignments (if sat)

Types

  • Int - Integers

  • Real - Real numbers

  • Bool - Boolean values

Operations

  • Arithmetic: +, -, *, /, mod

  • Comparison: =, <, >, <=, >=

  • Logic: and, or, not

  • Special: distinct (all different)

Transport Support

Currently supports:

  • stdio: For use with Claude Desktop and similar local clients

Planned:

  • HTTP/WebSocket: For web-based integrations

Troubleshooting

Common Issues

  1. Server not starting: Ensure Python and z3-solver are properly installed

  2. Permission denied: Make sure the main.py file is executable

  3. Import errors: Verify all dependencies are installed in the correct environment

Debug Mode

Run the server directly in the Inspector:

npx @modelcontextprotocol/inspector src/z3_mcp_server/main.py uv --directory /path/to/z3-mcp-server run main.py

Contributing

Contributions are welcome! Please:

  1. Fork the repository

  2. Create a feature branch

  3. Add tests for new functionality

  4. Submit a pull request

Available Tools

1 tool
solve_smt_lib2B

Solve the constraint problem provided in SMT-LIB2 format

ParametersJSON Schema
NameRequiredDescriptionDefault
problemYes

TDQS

B3.1/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations are provided, so the description carries the entire burden. It only says 'Solve the constraint problem' without revealing side effects, return value, or any restrictions. The behavior of the solver (e.g., whether it returns sat/unsat, a model, or has limits) is completely 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 a single, front-loaded sentence that wastes no words. It is appropriately concise for a simple tool, though it omits potentially useful details.

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?

With no output schema, no annotations, and only one sentence, the description leaves out critical context such as what the solver returns, any side effects, or error conditions. For a tool that processes user-supplied problems, this missing information limits a complete understanding.

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?

The schema provides zero description coverage for the single parameter 'problem'. The description adds some meaning by referencing 'SMT-LIB2 format', but it does not explicitly define the parameter's type or expected syntax beyond that. This partially compensates for the schema gap but not fully.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the action ('Solve') and the resource ('constraint problem'), specifying the input format as SMT-LIB2. This is a specific, non-tautological purpose statement that distinguishes the tool from a generic solver, even without sibling tools listed.

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 when a constraint problem is provided in SMT-LIB2 format, but it does not explicitly discuss when to use this tool versus alternatives or any prerequisites. Given no sibling tools exist, the implied context is acceptable but not explicit.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Install Server
RayrunBuild, deploy, and operate MCP servers without becoming an infrastructure team.ray.runAd

TDQS

A3.5/5.0
Disambiguation5/5

With only one tool, there is no possibility of confusion or overlap. The tool's purpose is singular and clear, so disambiguation is perfect.

Naming Consistency5/5

The tool name 'solve_smt_lib2' follows a clear verb_noun pattern, indicating the action and the input format. Consistency is trivially high with a single tool.

Tool Count3/5

The server has exactly one tool, which feels minimal for a solver domain. While it covers the core solve operation, a typical solver server might offer additional tools like model extraction or incremental assertions, making the count borderline.

Completeness4/5

The single tool accepts a full SMT-LIB2 script, which allows users to express a wide range of constraint problems including assertions, checks, and models. However, the lack of incremental interaction or separate utilities (e.g., parsing or model retrieval) is a minor gap.

Maintenance

ActivityInactive
ResponsivenessNo issues

Resources

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Related MCP Connectors

Related MCP Servers

  • USolver

    sdiehl
    A
    license
    B
    quality
    F
    maintenance
    A best-effort universal logic and numerical solver interface using MCP that implements the 'LLM sandwich' model to process queries, call dedicated solvers (ortools, cvxpy, z3), and verbalize results.
    7
    65
    Apache 2.0

  • Logic-LM MCP Server

    shipitsteven
    A
    license
    Not graded
    quality
    F
    maintenance
    Provides symbolic reasoning capabilities by converting natural language logical problems into Answer Set Programming (ASP) format and solving them using the Clingo solver. Enables users to perform formal logical reasoning, verify logical arguments, and get step-by-step explanations for complex logical problems.
    5
    MIT

  • Constrained Optimization MCP

    Sharmarajnish
    A
    license
    A
    quality
    C
    maintenance
    Enables solving complex combinatorial optimization problems with logical and numerical constraints through multiple solvers (Z3, CVXPY, HiGHS, OR-Tools). Specializes in portfolio optimization, scheduling, resource allocation, and constraint satisfaction problems.
    5
    5
    Apache 2.0

  • MCP Optimizer

    mrugankpednekar
    A
    license
    Not graded
    quality
    D
    maintenance
    Enables solving linear programming (LP) and mixed-integer linear programming (MILP) optimization problems through natural language, with built-in simplex and branch-and-cut solvers plus infeasibility diagnostics. Includes optional OR-Tools fallback for larger problems and supports parsing optimization problems from natural language descriptions.
    MIT

Latest Blog Posts

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/dsouflis/z3-solver-mcp-server'

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