Spec Driven Development
MCP Server that facilitates spec-driven development workflows, not just Vibe Coding.
在你的电脑上运行
MCP Z3 Prover
概览
作者提供的说明（英文原文）
MCP server exposing Z3 solver API
PopNx MCP 的三大支柱
这三项永远不会合并成一个分数：意见、测量和人气是不同的东西。
- 用户评价i暂无评价评价功能将在后续阶段与账户功能一起开放
- 我们的基础检查i1 项中通过 1 项依据公开信息检查；尚未扫描代码
- 使用情况i非常新↓ 23/周 · ★ –
它能帮你做什么
我们还没有为它写通俗的介绍。下面是我们从注册中心读取到的事实。
- 连接方式: 在你的电脑上运行
- 传输方式: stdio
- 分类: 其他
安装
选择你使用的 AI 应用，然后复制设置。
安装之前
- 基础检查：1 项中通过 1 项
- 在你的电脑上运行，拥有你的用户账户的权限（文件、网络、应用）。
- 注册中心没有列出需要填写的密钥。
你需要
- PyPI已安装 Python 的 uv（用于 uvx 命令）
你用的是哪个应用？
在上方选择你的应用。我们会记住它，下次按钮会显示“安装到 …”。
打开 Claude Desktop → Settings → Developer → Edit Config，把下面的内容粘贴到 claude_desktop_config.json
{
"mcpServers": {
"z3-prover": {
"command": "uvx",
"args": [
"mcp-z3-prover"
]
}
}
}在终端中运行这条命令
claude mcp add z3-prover -- uvx mcp-z3-prover或者自己复制设置
粘贴到项目中的 .cursor/mcp.json，或 ~/.cursor/mcp.json
{
"mcpServers": {
"z3-prover": {
"command": "uvx",
"args": [
"mcp-z3-prover"
]
}
}
}浏览器会先询问是否打开应用，然后应用会显示设置并请你确认。密钥的值会留空，由你自己填写。
或者自己复制设置
粘贴到项目中的 .vscode/mcp.json
{
"servers": {
"z3-prover": {
"type": "stdio",
"command": "uvx",
"args": [
"mcp-z3-prover"
]
}
}
}浏览器会先询问是否打开应用，然后应用会显示设置并请你确认。密钥的值会留空，由你自己填写。
这个服务器在你的电脑上运行，而 ChatGPT 只能连接互联网上的服务器。请选择其他应用。
你的选择通过 Cookie 保存在这台设备上，无需账户。
这些设置是根据作者在注册中心的条目生成的。如果 README 的写法不同，请以 README 为准。
它能做什么
它在你的电脑上运行；安装后，工具列表会显示在你的 AI 应用中。
基础检查i
我们检查的是任何人都能看到的信息；我们没有阅读代码。不适用的检查项不计入总数。 · 检查于 2026年11月8日
- ✓ 通过
作者与仓库一致
注册名称已通过 GitHub 账户 daedalus 验证，该账户拥有此仓库
- … 尚未检查
仍在维护
我们还没有从 GitHub 读取这个仓库
- … 尚未检查
有许可证
我们还没有从 GitHub 读取这个仓库
- – 不适用
端点有响应
它在你的电脑上运行，没有互联网端点
- – 不适用
使用 OAuth 登录
在你的电脑上运行，改用本地设置
- … 尚未检查
工具描述中没有隐藏指令
它在你的电脑上运行；我们只能读取互联网端点的工具列表
与“其他”中的其他服务器比较i
- 星标数多于此分类中其他 18513 个服务器的 0%
- 发布到注册中心的时间比此分类中其他 18513 个服务器的 4% 更新
- 基础检查结果等于或优于此分类中其他 18513 个服务器的 100%
与注册中心里这个分类中所有活跃的服务器比较。只有当发布者拥有该仓库时，星标数才计入。
常见问题
MCP Z3 Prover 安全吗？
它在 1 项适用的基础检查中通过了 1 项。我们没有阅读代码。在添加密钥或令牌之前，请先看看这个服务器要求哪些权限，并使用只具备所需权限的密钥。
它需要哪些密钥或代码？
注册中心没有列出必需的密钥，不过有些服务器会在首次使用时要求你登录。
它在我的电脑上运行还是在云端？
它在你的电脑上运行。你的 AI 应用会在需要时启动它，数据不会经过作者的服务器（除非它自己调用在线服务）。
它还在维护吗？
GitHub 仓库最后更新于–，最新版本（0.1.0）于7个月前进入注册中心。
哪些应用可以使用它？
支持 MCP 的应用，例如 Claude Desktop、Claude Code、Cursor 和 VS Code。你的电脑上还需要有 Python (uv)。
有什么可以替代它？
同一分类中有：Spec Driven Development, Remote Desktop Commander, Cape Winelands Visit Planner
替代选择
同一分类中其他作者的服务器，按星标数排序。
如何看卡片：↓ 每周下载量i★ GitHub 星标i三大支柱：评价 · 检查 · 使用情况i更新 = 最新版本发布到注册中心的时间i
Remote Desktop Commander
Remote Desktop Commander: use files, terminal and processes on your own computers from any AI app.
在云端运行✓ desktopcommander.app
Cape Winelands Visit Planner
Cape Winelands wine farm finder and day-route planner
在云端运行✓ aiagenttools.co.za
作者的 README
打开 README
按原文从作者的仓库复制。PopNx MCP 没有审查或背书其内容。HTML、图片和脚本已被移除。链接会离开本站。
mcp-z3-prover
MCP server exposing Z3 solver API
Install
pip install mcp-z3-proverUsage
from mcp_z3_prover import mcpRun the server
mcp.run()
Or from command line:
mcp-z3-proverMCP Tools
The server exposes the following tools:
- create_bool_var - Create a Boolean variable
- create_int_var - Create an Integer variable
- create_real_var - Create a Real variable
- create_int_constant - Create an integer constant
- create_real_constant - Create a real constant
- add_constraint - Add a constraint to the solver
- solve - Solve the current problem
- get_model_value - Get value of a variable from the model
- optimize - Solve with optimization objective
- reset_solver - Reset the solver state
- list_variables - List all created variables
Example
# Create variablescreate_int_var("x") create_int_var("y")
Add constraints
add_constraint("int:x + int:y == 10") add_constraint("int:x > 0") add_constraint("int:y > 0")
Solve
result = solve()
Returns: {"status": "sat", "model": {"x": "5", "y": "5"}}
Get specific values
x_val = get_model_value("int:x")
Integer Factorization Example
# Factor n = 4295229443 where n = p * q with q <= sqrt(n)create_int_var("p") create_int_var("q")
Add constraints
add_constraint("int:p * int:q == 4295229443") add_constraint("4295229443 > int:p") add_constraint("4295229443 > int:q") add_constraint("int:q <= 65537") # sqrt(4295229443) ≈ 65537 add_constraint("int:q > 1") add_constraint("int:p > 1") add_constraint("int:q % 2 != 0") # q is odd add_constraint("int:p % 2 != 0") # p is odd
Solve
result = solve()
Returns: {"status": "sat", "model": {"p": "65539", "q": "65537"}}
Verification: 65537 * 65539 = 4295229443
Development
git clone https://github.com/daedalus/mcp-z3-prover.gitcd mcp-z3-prover pip install -e ".[test]"
run tests
pytest
format
ruff format src/ tests/
lint
ruff check src/ tests/
type check
mypy src/
MCP Registration
mcp-name: io.github.daedalus/mcp-z3-prover