AI导哈

Z3定理求解器服务

通过标准化的MCP工具提供Z3定理证明器和约束求解器的访问服务，适用于AI助手和其他MCP客户端解决SMT-LIB问题。

  • by igorwwwwwwwwwwwwwwwwwwww
  • Go
  • 本地部署
  • 1 星标
  • 更新于
在 GitHub 查看 igorwwwwwwwwwwwwwwwwwwww/z3-mcp

使用说明

Z3 MCP服务器

一种模型上下文协议（MCP）服务器，通过标准化的MCP工具提供对Z3定理证明器和约束求解器的访问。

概述

该服务器通过MCP公开Z3的约束求解能力，允许AI助手和其他MCP客户端使用Z3定理证明器解决SMT-LIB问题。服务器包括用于安全执行的可选沙盒。

特性

  • Z3集成：在SMT-LIB输入上执行Z3约束求解器
  • 可配置超时：为求解器操作设置自定义超时值（默认值：10秒）
  • 跨平台沙盒：在macOS和Linux上的沙盒环境中运行Z3，以增强安全性
  • MCP协议：用于工具集成的标准模型上下文协议接口

先决条件

  • 转到1.24.4或更高版本
  • Z3定理证明器已安装在您的系统上
  • 对于沙盒：
    • macOS: sandbox-exec 命令（内置）
    • Linux: bwrap （气泡包装）包装

安装依赖项

Z3定理证明：

macOS（Homebrew）：

brew install z3

Linux（Ubuntu/Debian）：

sudo apt-get install z3

沙盒依赖性：

Linux（Ubuntu/Debian）：

sudo apt-get install bubblewrap

Linux（Fedora/RHEL）：

sudo dnf install bubblewrap

其他平台： 看 Z3官方安装指南

安装

  1. 克隆存储库：
git clone <repository-url>
cd z3-mcp
  1. 安装依赖项：
go mod download
  1. 构建服务器：
go build -o z3-mcp-server

用法

基本用法

在stdin/stdout上启动服务器（标准MCP模式）：

./z3-mcp-server

使用沙盒

启用沙盒以增强安全性：

./z3-mcp-server -sandbox

沙盒实现因平台而异：

  • macOS：用途 sandbox-exec 包括 z3.sb 个人资料
  • Linux：用途 bubblewrap 具有网络隔离和只读文件系统访问功能

码头工人

使用Docker构建和运行：

docker build -t z3-mcp .
docker run -i z3-mcp

带有Seccomp配置文件的Docker

为了增强安全性，请使用附带的seccomp配置文件运行容器：

docker run --security-opt seccomp=./seccomp-profile.json -i z3-mcp

seccomp配置文件基于Docker的官方默认配置文件，删除了所有与网络相关的系统调用，在保持完全容器兼容性的同时提供生产级安全性。

MCP工具接口

服务器提供一个MCP工具：

z3

对SMT-LIB输入执行Z3约束求解器。

参数：

  • input （string，必填）：求解SMT-LIB输入
  • timeout （数字，可选）：Z3求解器的超时时间（秒）（默认值：10）

SMT-LIB输入示例：

(declare-const x Int)
(declare-const y Int)
(assert (> x y))
(assert (= x 10))
(check-sat)
(get-model)

安全功能

沙箱

当使用启用时 -sandbox 标志Z3在受限沙箱中运行，该沙箱：

  • 拒绝网络访问
  • 限制文件系统写入
  • 只允许读取必要的文件
  • 将进程执行限制为仅Z3
  • 隔离进程命名空间（Linux）

平台特定实现：

  • macOS：用途 sandbox-exec 随着 z3.sb 个人资料
  • Linux：用途 bubblewrap 具有全面的文件系统和网络隔离
  • 码头工人：自定义seccomp配置文件(seccomp-profile.json)限制系统调用

许可证

MIT许可证-请参阅 许可证 文件以获取详细信息。

相关 MCP