Claude Desktop
Desktop · Freemium · Proprietary
Anthropic's official Claude AI desktop application. Supports MCP servers to extend functionality.
WindowsMacOS
Developer Tools · Education & Learning
z3_mcp
javergar/z3_mcp
This project demonstrates how to use the Z3 Theorem Prover with a functional programming approach to solve complex constraint satisfaction problems and analyze relationships between entities. It leverages the returns library for functional programming abstractions and exposes its capabilities through an MCP server.
Install
Client configuration
{
"mcpServers": {
"server": {
"command": "uv",
"args": [
"--directory",
"/path/to/your/z3_poc",
"run",
"z3_poc/server/main.py"
]
}
}
}- GitHub stars
- 1
- Author
- @javergar
- Category
- Developer Tools, Education & Learning
- License
- MIT
- Updated
- Oct 6, 2026
About z3_mcp
A Python implementation of abstactions over the Z3 Theorem Prover capabilities using functional programming principles, exposed through a Model Context Protocol (MCP) server.
Features
Constraint Satisfaction Problems: Solve complex problems with variables and constraints
Relationship Analysis: Analyze and infer relationships between entities
Functional Programming: Uses pure functions, immutable data structures, and monadic error handling
MCP Server: Exposes Z3 capabilities through a standardized interface
Tools (4)
solve_constraint_problem
Solves a constraint satisfaction problem with a full Problem model.
analyze_relationships
Analyzes relationships between entities with a full RelationshipQuery model.
simple_constraint_solver
A simpler interface for solving constraint problems without requiring the full Problem model.
simple_relationship_analyzer
A simpler interface for analyzing relationships without requiring the full RelationshipQuery model.
Details on this page are taken from the project's README. Open README
Supported clients
Clients mentioned in this server's README:
Cline
Desktop · Free · MIT
An AI coding assistant integrated into the IDE. Supports MCP servers for enhanced functionality.
VS Code GitHub Copilot
Desktop · Freemium · MIT
VS Code integrates MCP with GitHub Copilot through agent mode, allowing direct interaction with MCP-provided tools in your agentic coding workflow. Configure servers in Claude Desktop, workspace, or user settings, with guided MCP installation and secure handling of secrets in input variables to avoid leaking hardcoded keys.
Related MCP servers
Playwright
microsoft/playwright
Playwright is a framework for web automation and testing. It drives Chromium, Firefox, and WebKit with a single API — in your tests, in your scripts, and as a tool for AI agents.
repomix
yamadashy/repomix
Repomix is a tool that packs a codebase into an AI-friendly format, supporting local and remote repository processing and providing code compression, security checks and multiple output formats.
UI-TARS-desktop
bytedance/UI-TARS-desktop
TARS is ByteDance's multimodal AI agent stack, shipping two projects: Agent TARS (a CLI and Web UI agent built on MCP) and UI-TARS-desktop (a desktop GUI agent).
blender
ahujasid/blender-mcp
formerly blender-mcp — the PyPI package is now mcp-for-blender. Existing setups keep working; no config change is required. Read more.
Playwright Browser Automation
microsoft/playwright-mcp
A Model Context Protocol (MCP) server that provides browser automation capabilities using Playwright. This server enables LLMs to interact with web pages through structured accessibility snapshots, bypassing the need for screenshots or visually-tuned models.
2344
comet-ml/opik
Opik is the open-source LLM observability and evaluation platform for AI agent tracing, LLM evaluation, prompt management, and production monitoring. Built by Comet. Apache-2.0 licensed, free to self-host the full platform, with 20,000+ GitHub stars.