Related MCP Server Resources

Explore more AI models, providers, and integration options:

  • Explore AI Models
  • Explore AI Providers
  • Explore MCP Servers
  • LangDB Pricing
  • Documentation
  • AI Industry Blog
  • GIS Data Conversion MCP
  • Steel Puppeteer
  • Chrome Debug MCP Server
  • PCM
  • GHAS MCP server GitHub Advanced Security
Back to MCP Servers
MCP-RoCQ

MCP-RoCQ

Public
angrysky56/mcp-rocq

Provides advanced logical reasoning through Model Context Protocol integration with the Coq proof assistant, enabling automated dependent type checking, inductive type definitions, property proving with custom tactics and automation, and robust error handling.

python
0 tools
May 29, 2025
Updated Jun 4, 2025

Supercharge Your AI with MCP-RoCQ

MCP Server

Unlock the full potential of MCP-RoCQ through LangDB's AI Gateway. Get enterprise-grade security, analytics, and seamless integration with zero configuration.

Unified API Access
Complete Tracing
Instant Setup
Get Started Now

Free tier available • No credit card required

Instant Setup
99.9% Uptime
10,000+Monthly Requests

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

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

  1. Install dependencies:
pip install -r requirements.txt

Usage

The server provides three main capabilities:

1. Type Checking

{ "tool": "type_check", "args": { "term": "", "expected_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": "", "tactics": [""], "use_automation": true } }

License

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

Publicly Shared Threads0

Discover shared experiences

Shared threads will appear here, showcasing real-world applications and insights from the community. Check back soon for updates!

Share your threads to help others
Related MCPs5
  • GIS Data Conversion MCP
    GIS Data Conversion MCP

    Provides Model Context Protocol (MCP) integration enabling large language models to perform advanced...

    9 tools
    Added May 30, 2025
  • Steel Puppeteer
    Steel Puppeteer

    Model Context Protocol server enabling advanced browser automation with Puppeteer, offering web navi...

    Added May 30, 2025
  • Chrome Debug MCP Server
    Chrome Debug MCP Server

    Model Context Protocol server enabling advanced browser automation with Playwright, featuring multi-...

    13 tools
    Added May 30, 2025
  • PCM
    PCM

    Provides advanced reverse engineering capabilities through Model Context Protocol, including functio...

    24 tools
    Added May 30, 2025
  • GHAS MCP server GitHub Advanced Security
    GHAS MCP server GitHub Advanced Security

    Provides Model Context Protocol (MCP) integration for GitHub Advanced Security by enabling read-only...

    Added May 30, 2025