Dafny Verifier MCP server

This server implements the Model Context Protocol (MCP) for the Dafny programming language, enabling verification capabilities when working with Claude AI models. It allows you to send Dafny code to be verified as part of your interactions with Claude.

Requirements

Before setting up the Dafny MCP server, you'll need to install:

• Dafny: A programming language and verification system
• MCP Python SDK: The Model Context Protocol SDK

Installing Dafny

On macOS, you can install Dafny using Homebrew:

brew install dafny

For other operating systems, please refer to the official Dafny installation instructions.

Installation

To install the Dafny MCP server, follow these steps:

1. Install the MCP CLI using uv pip:

uv pip install "mcp[cli]"

2. Install the MCP server:

mcp install mcp.py

3. Start the development server:

mcp dev mcp.py

Usage

Once the server is running, you can interact with it using Claude. The server will verify your Dafny code and provide feedback on correctness.

Example Workflow

1. Start the MCP server as shown above
2. In your conversation with Claude, you can now send Dafny code for verification
3. Claude will use the MCP server to verify the code and respond with verification results

Verification Results

The server will return information about:

• Whether the code passes verification
• Any errors or warnings detected
• Verification conditions that were checked

You can continue to interact with Claude, making adjustments to your Dafny code based on the verification feedback.

How to install this MCP server

For Claude Code

To add this MCP server to Claude Code, run this command in your terminal:

claude mcp add-json "dafny-verifier" '{"command":"python","args":["-m","mcp.py"]}'

See the official Claude Code MCP documentation for more details.

For Cursor

There are two ways to add an MCP server to Cursor. The most common way is to add the server globally in the ~/.cursor/mcp.json file so that it is available in all of your projects.

If you only need the server in a single project, you can add it to the project instead by creating or adding it to the .cursor/mcp.json file.

Adding an MCP server to Cursor globally

To add a global MCP server go to Cursor Settings > Tools & Integrations and click "New MCP Server".

When you click that button the ~/.cursor/mcp.json file will be opened and you can add your server like this:

{
    "mcpServers": {
        "dafny-verifier": {
            "command": "python",
            "args": [
                "-m",
                "mcp.py"
            ]
        }
    }
}

Adding an MCP server to a project

To add an MCP server to a project you can create a new .cursor/mcp.json file or add it to the existing one. This will look exactly the same as the global MCP server example above.

How to use the MCP server

Once the server is installed, you might need to head back to Settings > MCP and click the refresh button.

The Cursor agent will then be able to see the available tools the added MCP server has available and will call them when it needs to.

You can also explicitly ask the agent to use the tool by mentioning the tool name and describing what the function does.

For Claude Desktop

To add this MCP server to Claude Desktop:

1. Find your configuration file:

• macOS: ~/Library/Application Support/Claude/claude_desktop_config.json
• Windows: %APPDATA%\Claude\claude_desktop_config.json
• Linux: ~/.config/Claude/claude_desktop_config.json

2. Add this to your configuration file:

{
    "mcpServers": {
        "dafny-verifier": {
            "command": "python",
            "args": [
                "-m",
                "mcp.py"
            ]
        }
    }
}

3. Restart Claude Desktop for the changes to take effect