使用说明

项目简介

本项目是一个基于 Model Context Protocol (MCP) 的服务器实现，它将 Dafny 验证器包装成一个可以通过 MCP 协议调用的工具。这意味着你可以通过支持 MCP 协议的 LLM 客户端，向这个服务器发送 Dafny 代码，并获得 Dafny 验证器的验证结果。

主要功能点

• Dafny 代码验证: 提供 'dafny_verifier' 工具，接收 Dafny 代码字符串作为输入，调用本地安装的 Dafny 验证器进行代码验证，并返回验证结果（标准输出的截取）。
• MCP 工具注册: 使用 MCP Python SDK 注册 'dafny_verifier' 工具，使其可以通过 MCP 协议被客户端发现和调用。
• 快速启动: 利用 'fastmcp' 简化服务器搭建，快速将 Dafny 验证功能暴露为 MCP 服务。

安装步骤

1. 安装 Dafny 验证器: 确保你的本地环境中已经安装了 Dafny 验证器。例如，在 macOS 上可以使用 'brew install dafny' 命令安装。
2. 安装 MCP Python SDK 和 CLI 工具: 运行命令 'uv pip install "mcp[cli]"' 安装 MCP Python SDK 及其命令行工具。
3. 安装 MCP 服务器: 在仓库目录下，运行 'mcp install mcp.py' 命令安装此 MCP 服务器。

服务器配置

MCP 客户端需要配置以下 JSON 格式的信息来连接到 Dafny MCP 服务器。

{
  "serverName": "Dafny",  // 服务器名称，由 FastMCP("Dafny") 定义
  "command": "mcp",      // 启动服务器的命令，使用 mcp CLI 工具
  "args": ["dev", "mcp.py"] // 启动参数，使用 mcp dev 模式运行 mcp.py 文件
}

配置参数说明:

• 'serverName': 服务器的名称，客户端可以使用此名称来识别和连接服务器。本例中为代码中定义的 "Dafny"。
• 'command': 启动服务器的可执行命令。这里使用 'mcp'，这是 MCP Python SDK 提供的命令行工具。
• 'args': 传递给 'command' 的参数列表。'dev mcp.py' 表示使用 'mcp' 工具以开发模式运行 'mcp.py' 文件，启动 MCP 服务器。

基本使用方法

1. 启动 MCP 服务器: 按照上述服务器配置，使用 MCP 客户端配置的启动命令，客户端会自动启动 'mcp dev mcp.py' 命令来启动 Dafny MCP 服务器。
2. 客户端调用 'dafny_verifier' 工具: 在 MCP 客户端中，你可以通过工具名称 'dafny_verifier' 调用该工具。你需要提供 Dafny 代码字符串作为工具的输入参数 'code'。
3. 获取验证结果: 服务器会调用本地 Dafny 验证器验证代码，并将验证结果（标准输出的前1000个字符）作为字符串返回给客户端。

示例 (MCP 客户端请求，伪代码):

// 假设 client 是 MCP 客户端实例
response = client.call_tool("dafny_verifier", {"code": "method Main() {\n  assert 1 == 1;\n}"})
print(response) // 打印验证结果

请注意，此服务器依赖于本地 Dafny 验证器的安装和环境变量配置。客户端需要确保能够连接到运行中的 MCP 服务器，并正确处理服务器返回的 JSON-RPC 响应。