What is Mcp Rocq

mcp-rocq is a Model Context Protocol server that integrates with the Coq proof assistant, providing advanced logical reasoning capabilities such as automated dependent type checking, inductive type definitions, and property proving.

Use cases

Use cases for mcp-rocq include verifying complex type systems in programming languages, defining and checking custom inductive data types, and proving logical properties in formal specifications.

How to use

To use mcp-rocq, first install the Coq Platform version 8.19, clone the repository, set up a virtual environment, and install the required dependencies. Then, configure the server with the appropriate paths for Coq and the repository, and utilize its main capabilities for type checking, inductive types, and property proving via JSON commands.

Key features

Key features include automated dependent type checking, inductive type definition, property proving with custom tactics, XML protocol integration for structured communication, and rich error handling for type errors and failed proofs.

Where to use

mcp-rocq is suitable for formal verification, theorem proving, and any domain requiring rigorous logical reasoning and type checking, such as software development, mathematical proofs, and research in formal methods.

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

1. 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

2. 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.

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

3. 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.