Advertise
MCP.so
Sign In

MCP-RoCQ (Coq Reasoning Server)

@angrysky56

Repository

Basic information

Category

Reasoning

Transports

stdio

Author

angrysky56

About MCP-RoCQ

RoCQ (Coq Reasoning Server)

#coq#claude#mcp-server

MCP-RoCQ config

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

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

MCP-RoCQ tools

Tool list not available yet

This listing does not currently have a tool list to display. This does not mean the server has no tools; check its documentation for supported capabilities.

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

Frequently asked questions

1

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.

2

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.

3

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

4

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.

5

How is communication with Coq handled?

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

Comments

More Reasoning MCP servers

IntelliNode Medical Use Cases

Barqawiz

Multi-Agent AI Orchestration Workshop

9

AWorld: Advancing Agentic AI

inclusionAI

Search, understand, reproduce, and improve an idea with ease

1.2K

🐢🚀 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 Resource Discovery

neuronto

Neuronto Agentic Resource Discovery (ARD) Index. Federated search across every public ARD registry, plus a verified tool index read from each MCP server's own tools/list, hybrid lexical and semantic retrieval, and ARD-Bench.

60

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
Advertise