MCP-RoCQ

MCP-RoCQ (Coq Reasoning Server)

Currently shows tools but Claude can't use it properly for some reason- invalid syntax generally seems the issue but there could be something else.

There may be a better way to set this up with the coq cli or something. Anyone want to try and fix it who knows what they are doing would be great.

MCP-RoCQ is a Model Context Protocol server that 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.

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

Install the Coq Platform 8.19 (2024.10)

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

https://github.com/coq/platform

Clone this repository:

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

cd to the repo

uv venv
./venv/Scripts/activate
uv pip install -e .

JSON for the Claude App or mcphost config- set your paths according to how you installed coq and the repository.

    "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"
      ]
    },

This might work- I got it going with uv and most of this could be hallucinatory though:

Install dependencies:

pip install -r requirements.txt

Usage

The server provides three main capabilities:

1. Type Checking

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

2. Inductive Types

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

3. Property Proving

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

License

This project is licensed under the MIT License - see the LICENSE file for details.

This server cannot be installed

security - not tested

license - permissive license

quality - not tested

How are these scores calculated?

local-only server

The server can only run on the client's local machine because it depends on local resources.

MCP-RoCQ 与 Coq 证明助手集成，通过 XML 协议通信实现自动依赖类型检查、归纳类型定义和属性证明。

Related Resources

Reddit Discussion about this server

Related MCP Servers

MCP-Logic
angrysky56
-
security
A
license
-
quality
MCP-Logic is a server that provides AI systems with automated reasoning capabilities, enabling logical theorem proving and model verification using Prover9/Mace4 through a clean MCP interface.
Last updated -
31
MIT License
onyx-mcp-server
lupuletic
A
security
A
license
A
quality
Connect your MCP-compatible clients to Onyx AI knowledge bases for enhanced semantic search and chat capabilities. Retrieve relevant context from your documents seamlessly, enabling powerful interactions and comprehensive answers. Streamline knowledge management and improve access to information acr
Last updated -
2
297
16
MIT License
Chain of Thought MCP Server
beverm2391
-
security
F
license
-
quality
An MCP server that uses Groq's API to expose raw chain-of-thought tokens from Qwen's qwq model, enabling LLMs to think step-by-step before responding.
Last updated -
11
Calculator MCP Server
mzdz
-
security
F
license
-
quality
Provides basic arithmetic operations and advanced mathematical functions through the Model Context Protocol (MCP), with features like calculation history tracking and expression evaluation.
Last updated -

View all related MCP servers

MCP-RoCQ

MCP-RoCQ (Coq Reasoning Server)

Currently shows tools but Claude can't use it properly for some reason- invalid syntax generally seems the issue but there could be something else.

Features

Installation

JSON for the Claude App or mcphost config- set your paths according to how you installed coq and the repository.

This might work- I got it going with uv and most of this could be hallucinatory though:

Usage

1. Type Checking

2. Inductive Types

3. Property Proving

License

Related Resources

Related MCP Servers

MCP-Logic

onyx-mcp-server

Chain of Thought MCP Server

Calculator MCP Server

Appeared in Searches

New MCP Servers

MCP directory API