mcp-rocq

mcp-rocq

4
developer_tools

MCP-RoCQ is a Model Context Protocol server designed to work with the Coq proof assistant, enabling advanced logical reasoning through type checking, inductive definitions, and property proving. It provides an environment for automated and semi-interactive development of proofs.

MCP-RoCQ (Coq Reasoning Server)

MCP-RoCQ is a Model Context Protocol server that integrates with the Coq proof assistant to provide advanced logical reasoning capabilities. Key features include:

  • Automated dependent type checking: verifying terms against complex dependent types.
  • Inductive type definitions: defining and verifying custom data types.
  • Property proving: leveraging custom tactics and automation for logical proofs.
  • XML protocol integration and rich error handling for structured communication and feedback.

Installation

  1. Install the Coq Platform 8.19.
  2. Clone the repository from GitHub.
  3. Set up a virtual environment and install dependencies.

Usage

The server offers type checking, inductive type definitions, and property proving capabilities.