Provides a Dafny-based MCP server to verify models and contexts within Claude workflows.
Configuration
View docs{
"mcpServers": {
"dafny_mcp": {
"command": "mcp",
"args": [
"dev",
"mcp.py"
],
"env": {
"DAFNY_PATH": "YOUR_DAFNY_PATH",
"MCP_SDK_PATH": "/path/to/mcp/sdk",
"MCP_SDK": "YOUR_MCP_SDK_PATH"
}
}
}
}Dafny-mcp is a Model Context Protocol (MCP) server that leverages the Dafny verifier to work with Claude. It enables you to verify models and interactions in a structured MCP workflow, providing automated checks and a concrete runtime you can connect to with an MCP client.
You run the Dafny-mcp server locally and then connect your MCP client to it to perform verification tasks. Start the development server and use your client to request verifications, run checks, and receive feedback from the Dafny-based verifier. This setup is useful for iterating on models and quickly validating your context-related proofs.
Typical usage pattern: - Start the local MCP server - Connect your MCP client to the server URL or stdio interface - Submit model/context checks and interpret the results in your workflow - Iterate by updating your model and re-running checks to see updated results.
mcp install mcp.py
mcp dev mcp.py
```
This sequence installs the MCP script and starts the server in development mode, ready to accept client requests.Prerequisites you should have before installing Dafny-mcp:
- Dafny installed locally (commonly via a package manager; for macOS, you can install with brew: brew install dafny).
- The MCP Python SDK available for your environment.
uv pip install "mcp[cli]"
mcp install mcp.py
mcp dev mcp.pyThis server relies on the Dafny verifier and the MCP Python SDK. Ensure you have Dafny installed and accessible in your PATH, and that you can run Python-based MCP tooling as shown in the installation steps.