We are excited to announce the release of QCP v2.0beta! This update focuses on bridging the gap between Large Language Models (LLMs) and formal verification. By introducing qcp-mcp and rocq-mcp, we have enabled AI agents to interact directly with QCP, allowing them to autonomously write annotations and construct rigorous Rocq proofs. This release marks a significant step towards automating the formal verification workflow using the power of generative AI.
What's New
qcp-mcp: We have implemented a Model Context Protocol (MCP) server, providing a standardized interface for AI to execute QCP commands and retrieve error logs.rocq-mcp: We introducedrocq-mcpto enable the automatic generation of Rocq proofs. This tool allows AI agents to autonomously construct and verify theorems, significantly reducing the manual effort required for formal verification.