MCP-RoCQ (Coq Reasoning Server)

@angrysky56

代码仓库

基本信息

分类

推理

传输方式

stdio

作者

angrysky56

关于 MCP-RoCQ

RoCQ (Coq Reasoning Server)

#coq#claude #mcp-server

MCP-RoCQ 配置

使用下面的配置,将此服务器添加到你的 MCP 客户端。

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

MCP-RoCQ 工具

工具列表暂未提供

当前收录暂时没有可展示的工具列表，不代表服务没有工具。请查阅项目文档了解支持的能力。

工具是从 README 中自动提取的。维护者可以在 ## Tools 标题下列出工具,即可填充这部分内容。

概览

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

常见问题

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.

推理分类下的更多 MCP 服务器

Agentic Radar

splx-ai

A security scanner for your LLM agentic workflows

993

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

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

Code Reasoning MCP Server

mettamatt

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

255

ArduPilot MCP Server Sandbox

hfujikawa77

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