drio
Open app

MCP-RoCQ (Coq Reasoning Server)

Source

RoCQ (Coq Reasoning Server)

Catalog onlyCatalog onlySTDIO

Overview

MCP-RoCQ is a Model Context Protocol server that provides advanced logical reasoning capabilities through integration with the Coq proof assistant, enabling automated dependent type checking, inductive type definitions, and property proving.

To use MCP-RoCQ, install the Coq Platform, clone the repository, set up your environment, and use the provided JSON commands for type checking, defining inductive types, and proving properties.

  • Automated Dependent Type Checking - Inductive Type Definition - Property Proving - XML Protocol Integration - Rich Error Handling
  1. Verifying complex mathematical proofs.
  2. Defining and checking custom data types in Coq.
  3. Automating logical property proofs in software verification.

Add to your AI client

Use these steps to connect MCP-RoCQ (Coq Reasoning Server) in Cursor, Claude, VS Code, and other MCP-compatible apps. The same JSON appears in the Use with menu above for one-click copy.

Cursor

Add this to your .cursor/mcp.json file in your project root, then restart Cursor.

.cursor/mcp.json

{
  "mcpServers": {
    "mcp-rocq-angrysky56": {
      "command": "npx",
      "args": [
        "-y",
        "@modelcontextprotocol/server-mcp-rocq-angrysky56"
      ]
    }
  }
}

Claude Desktop

Add this server entry to the mcpServers object in your Claude Desktop config, then restart the app.

~/Library/Application Support/Claude/claude_desktop_config.json (macOS) or %APPDATA%\Claude\claude_desktop_config.json (Windows)

{
  "mcpServers": {
    "mcp-rocq-angrysky56": {
      "command": "npx",
      "args": [
        "-y",
        "@modelcontextprotocol/server-mcp-rocq-angrysky56"
      ]
    }
  }
}

Claude Code

Add this to your project's .mcp.json file. Claude Code will detect it automatically.

.mcp.json (project root)

{
  "mcpServers": {
    "mcp-rocq-angrysky56": {
      "command": "npx",
      "args": [
        "-y",
        "@modelcontextprotocol/server-mcp-rocq-angrysky56"
      ]
    }
  }
}

VS Code (Copilot)

Add this to your .vscode/mcp.json file. Requires the GitHub Copilot extension with MCP support enabled.

.vscode/mcp.json

{
  "servers": {
    "mcp-rocq-angrysky56": {
      "type": "stdio",
      "command": "npx",
      "args": [
        "-y",
        "@modelcontextprotocol/server-mcp-rocq-angrysky56"
      ]
    }
  }
}

Windsurf

Add this to your Windsurf MCP config file, then restart Windsurf.

~/.codeium/windsurf/mcp_config.json

{
  "mcpServers": {
    "mcp-rocq-angrysky56": {
      "command": "npx",
      "args": [
        "-y",
        "@modelcontextprotocol/server-mcp-rocq-angrysky56"
      ]
    }
  }
}

Cline

Open Cline settings, navigate to MCP Servers, and add this server configuration.

Cline MCP Settings (via UI)

{
  "mcpServers": {
    "mcp-rocq-angrysky56": {
      "command": "npx",
      "args": [
        "-y",
        "@modelcontextprotocol/server-mcp-rocq-angrysky56"
      ]
    }
  }
}

FAQ

What is the Coq proof assistant?

Coq is a formal proof management system that provides a formal language to write mathematical definitions and theorems.

How do I install MCP-RoCQ?

Follow the installation instructions in the documentation, including installing the Coq Platform and cloning the repository.

Can MCP-RoCQ handle all types of logical proofs?

Yes, it is designed to handle a wide range of logical proofs and type checking.7:["$","div",null,{"className":"container mx-auto flex flex-col gap-4","children":["$L26","$L27",["$","$L28",null,{"currentProject":{"id":1544,"uuid":"ea4405ed-0674-4acc-abb0-e516b2ae0ea9","name":"mcp-rocq","title":"MCP-RoCQ (Coq Reasoning Server)","description":"RoCQ (Coq Reasoning Server)","avatar_url":"https://avatars.githubusercontent.com/u/113643118?v=4","created_at":"2025-02-20T16:22:15.496Z","updated_at":"2025-02-23T07:12:22.931Z","status":"created","author_name":"angrysky56","author_avatar_url":"https://avatars.githubusercontent.com/u/113643118?v=4","tags":"coq,claude,mcp-server","category":"research-and-data","is_featured":false,"sort":1,"url":"https://github.com/angrysky56/mcp-rocq","target":"_self","content":"$29","summary":"$2a","img_url":null,"type":null,"metadata":null,"user_uuid":null,"tools":null,"sse_url":null,"sse_provider":null,"sse_params":null,"is_official":false,"server_command":null,"server_params":null,"server_config":null,"allow_call":false,"is_innovation":false,"is_dxt":false,"dxt_manifest":null,"dxt_file_url":null,"is_audit":false},"randomProjects":[],"currentServerKey":"$undefined"}]]}]

Research and data