Skip to content

QCP-v2.0beta

Pre-release
Pre-release

Choose a tag to compare

View all tags
@yashen32768 yashen32768 released this 29 Mar 18:44
· 18 commits to main since this release
v2.0beta
b8e6772

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 introduced rocq-mcp to 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.
Assets 2
Loading