home / mcp / rocq mcp server

RoCQ MCP Server

RoCQ (Coq Reasoning Server)

Installation

Add the following to your MCP client configuration file.

Configuration

{
  "mcpServers": {
    "angrysky56-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"
      ]
    }
  }
}

MCP-RoCQ (Coq Reasoning Server) provides advanced logical reasoning capabilities by integrating with the Coq proof assistant. It enables automated dependent type checking, inductive type definitions, and property proving, all accessible through a lightweight MCP client workflow. This server is useful when you want to perform formal reasoning tasks within your development or research environment and receive structured feedback on types and proofs.

How to use

You interact with the RoCQ MCP server through an MCP client you already use in your workflow. The server exposes three core capabilities you can leverage: dependent type checking of terms against complex types, inductive type definitions with automatic verification, and property proving using a mix of tactics and automation. When you submit a request, you specify the tool you want to run and provide the relevant arguments, such as the term to check, the name of an inductive type with its constructors, or a logical statement to prove along with a tactic sequence.

How to install

Prerequisites include a Coq proof environment and a Python-based MCP runner. Follow these steps to set up RoCQ locally.

# 1) Install the Coq Platform (version 8.19, 2024.10)
# This provides the Coq proof environment used by RoCQ
# Follow the platform installation method appropriate for your OS

# 2) Clone RoCQ repository
git clone https://github.com/angrysky56/mcp-rocq.git

# 3) Change into the repository
cd mcp-rocq

# 4) Create and activate a Python virtual environment (uv tooling is assumed)
uv venv
# On Windows you might activate with: .\venv\Scripts\activate

# 5) Install the RoCQ package in editable mode
uv pip install -e .
```

With these steps complete, you can proceed to configure and run RoCQ using your MCP client. The client will connect to RoCQ through a local stdio configuration that RoCQ supports for in-process usage.

Configuration for your MCP client

RoCQ can be started as a local stdio server. Use the provided runtime command and arguments to launch the server from your MCP client. The following configuration is an explicit example that you should adapt to your local paths and environment.

{
  "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"
    ]
  }
}
```

Adapt the paths to match your system layout. This startup pattern uses a local runtime to host RoCQ as an MCP server that your client can communicate with directly.

Available tools

type_check

Automated dependent type checking that verifies a term against a given dependent type within a context.

define_inductive

Definition and automatic verification of custom inductive data types with specified constructors.

prove_property

Prove logical properties using a sequence of tactics and optional automation.

xml_protocol_integration

Structured communication with Coq via an XML-based protocol for reliable data exchange.

rich_error_handling

Detailed feedback for type errors and failed proofs to guide corrections.