MCP.so
Sign In

MCP-RoCQ (Coq Reasoning Server)

@angrysky56

Repository

About MCP-RoCQ (Coq Reasoning Server)

RoCQ (Coq Reasoning Server)

#coq#claude#mcp-server

Config

Add this server to your MCP-compatible client using the configuration below.

{
  "mcpServers": {
    "mcp-rocq": {
      "command": "uv",
      "args": [
        "venv"
      ]
    }
  }
}

Tools

No tools detected

We auto-extract tools from the README. The maintainer can list them under a ## Tools heading to populate this section.

Overview

What is MCP-RoCQ?

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.

How to use MCP-RoCQ?

Install the Coq Platform 8.19 (2024.10), clone the repository, set up a uv virtual environment, install the package with uv pip install -e ., and configure the server with the --coq-path and --lib-path arguments in your MCP client JSON. The server exposes three tools: type_check, define_inductive, and prove_property.

Key features of MCP-RoCQ

  • Automated dependent type checking
  • Inductive type definition with verification
  • Property proving using custom tactics and automation
  • XML protocol integration for structured communication with Coq
  • Rich error handling for type errors and failed proofs

Use cases of MCP-RoCQ

  • Verify terms against complex dependent types in Coq
  • Define and automatically verify custom inductive data types
  • Prove logical properties using automated or custom tactic sequences

FAQ from MCP-RoCQ

What does MCP-RoCQ integrate with?

It integrates with the Coq proof assistant (Coq Platform 8.19, 2024.10 release) through the coqtop executable and Coq library paths.

What dependencies are required?

You need the Coq Platform 8.19, Python, uv, and the cloned repository. A JSON configuration example shows paths to coqtop.exe and the Coq library directory.

What tools does the server provide?

Three main tools: type_check (verify a term against an expected type), define_inductive (define and verify inductive types), and prove_property (prove a logical statement using tactics and optional automation).

Is the server fully functional?

The README notes that while tools are shown, Claude may not use them properly due to invalid syntax, and the author suggests others may want to fix the setup. The server is experimental and contributions are welcome.

How is communication with Coq handled?

The server uses XML protocol integration for reliable structured communication with Coq.

Frequently asked questions

What does MCP-RoCQ integrate with?

It integrates with the Coq proof assistant (Coq Platform 8.19, 2024.10 release) through the `coqtop` executable and Coq library paths.

What dependencies are required?

You need the Coq Platform 8.19, Python, uv, and the cloned repository. A JSON configuration example shows paths to `coqtop.exe` and the Coq library directory.

What tools does the server provide?

Three main tools: `type_check` (verify a term against an expected type), `define_inductive` (define and verify inductive types), and `prove_property` (prove a logical statement using tactics and optional automation).

Is the server fully functional?

The README notes that while tools are shown, Claude may not use them properly due to invalid syntax, and the author suggests others may want to fix the setup. The server is experimental and contributions are welcome.

How is communication with Coq handled?

The server uses XML protocol integration for reliable structured communication with Coq.

Comments

Basic information

Category

Reasoning

Transports

stdio

Author

angrysky56

More Reasoning MCP servers

🐢🚀 Node.js Sandbox MCP Server

alfonsograziano

A Node.js–based Model Context Protocol server that spins up disposable Docker containers to execute arbitrary JavaScript.

154

Agentic Tools MCP Server

Pimzino

A comprehensive Model Context Protocol (MCP) server providing AI assistants with powerful task management and agent memories capabilities with project-specific storage.

87

Agentic MCP Client

peakmojo

A standalone agent runner that executes tasks using MCP (Model Context Protocol) tools via Anthropic Claude, AWS BedRock and OpenAI APIs. It enables AI agents to run autonomously in cloud environments and interact with various systems securely.

41

n8n Workflow Builder MCP Server

makafeli

AI assistant integration for n8n workflow automation through Model Context Protocol (MCP). Connect Claude Desktop, ChatGPT, and other AI assistants to n8n for natural language workflow management.

530

quarkus-langchain4j-workshop

quarkusio

Quarkus LangChain4J Workshop that demonstrates both single AI service capabilities and Agentic AI orchestration

91