mcp-rocq

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.

type_check

Check if the term meets the expected type

define_inductive

Define the induction type and verify

prove_property

Proof logic properties