RoCQ MCP server

The MCP-RoCQ server provides advanced logical reasoning capabilities through integration with the Coq proof assistant. It enables automated dependent type checking, inductive type definitions, and property proving with both custom tactics and automation through a structured Model Context Protocol interface.

Features

• Automated Dependent Type Checking: Verify terms against complex dependent types
• Inductive Type Definition: Define and automatically verify custom inductive data types
• Property Proving: Prove logical properties using custom tactics and automation
• XML Protocol Integration: Reliable structured communication with Coq
• Rich Error Handling: Detailed feedback for type errors and failed proofs

Installation

Prerequisites

First, you need to install the Coq Platform 8.19 (2024.10). Coq is a formal proof management system that provides a formal language to write mathematical definitions, executable algorithms, and theorems.

You can download and install it from: https://github.com/coq/platform

Installing MCP-RoCQ

1. Clone the repository:

git clone https://github.com/angrysky56/mcp-rocq.git

2. Navigate to the repository directory:

cd mcp-rocq

3. Create and activate a virtual environment using uv:

uv venv
./venv/Scripts/activate

4. Install the package in development mode:

uv pip install -e .

Alternatively, you can install dependencies using pip:

pip install -r requirements.txt

Configuration

To configure MCP-RoCQ with Claude App or mcphost, you need to create a JSON configuration. Adjust the paths according to your Coq installation and repository location:

{
  "mcp-rocq": {
    "command": "uv",
    "args": [
      "--directory",
      "F:/GithubRepos/mcp-rocq",
      "run",
      "mcp_rocq",
      "--coq-path",
      "F:/Coq-Platform~8.19~2024.10/bin/coqtop.exe",
      "--lib-path",
      "F:/Coq-Platform~8.19~2024.10/lib/coq"
    ]
  }
}

Usage

The MCP-RoCQ server provides three main capabilities that you can access via JSON requests:

Type Checking

Use this capability to verify terms against expected types:

{
    "tool": "type_check",
    "args": {
        "term": "<term to check>",
        "expected_type": "<type>",
        "context": ["relevant", "modules"] 
    }
}

Defining Inductive Types

Create custom inductive data types with this capability:

{
    "tool": "define_inductive",
    "args": {
        "name": "Tree",
        "constructors": [
            "Leaf : Tree",
            "Node : Tree -> Tree -> Tree"
        ],
        "verify": true
    }
}

Property Proving

Prove logical properties using tactics and automation:

{
    "tool": "prove_property",
    "args": {
        "property": "<statement>",
        "tactics": ["<tactic sequence>"],
        "use_automation": true
    }
}

Each of these capabilities accepts specific parameters as shown in the examples above. The server responds with results, including whether operations succeeded or failed, along with detailed error information when necessary.

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 "mcp-rocq" '{"command":"uv","args":["--directory","F:/GithubRepos/mcp-rocq","run","mcp_rocq","--coq-path","F:/Coq-Platform~8.19~2024.10/bin/coqtop.exe","--lib-path","F:/Coq-Platform~8.19~2024.10/lib/coq"]}'

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": {
        "mcp-rocq": {
            "command": "uv",
            "args": [
                "--directory",
                "F:/GithubRepos/mcp-rocq",
                "run",
                "mcp_rocq",
                "--coq-path",
                "F:/Coq-Platform~8.19~2024.10/bin/coqtop.exe",
                "--lib-path",
                "F:/Coq-Platform~8.19~2024.10/lib/coq"
            ]
        }
    }
}

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": {
        "mcp-rocq": {
            "command": "uv",
            "args": [
                "--directory",
                "F:/GithubRepos/mcp-rocq",
                "run",
                "mcp_rocq",
                "--coq-path",
                "F:/Coq-Platform~8.19~2024.10/bin/coqtop.exe",
                "--lib-path",
                "F:/Coq-Platform~8.19~2024.10/lib/coq"
            ]
        }
    }
}

3. Restart Claude Desktop for the changes to take effect