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

Basic information

Category

Reasoning

Transports

stdio

Publisher

angrysky56

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.

Comments

More Reasoning MCP servers

IntelliNode Medical Use Cases

Barqawiz

Multi-Agent AI Orchestration Workshop

9

ArduPilot MCP Server Sandbox

hfujikawa77

ArduPilotドローンをAIエージェントから操作するMCPサーバーです。

9

Part 1. Real-Time LangGraph Agent with MCP Tool Execution

junfanz1

This project demonstrates a decoupled real-time agent architecture that connects LangGraph agents to remote tools served by custom MCP (Modular Command Protocol) servers. The architecture enables a flexible and scalable multi-agent system where each tool can be hosted independent

27

Code Reasoning MCP Server

mettamatt

A code reasoning MCP server, a fork of sequential-thinking

255

End-to-End Agentic AI Automation Lab

MDalamin5

This repository contains hands-on projects, code examples, and deployment workflows. Explore multi-agent systems, LangChain, LangGraph, AutoGen, CrewAI, RAG, MCP, automation with n8n, and scalable agent deployment using Docker, AWS, and BentoML.

83