LatestStable
QCP-v2.1.0
QCP-v2.1.0
We are pleased to announce QCP v2.1.0. This release is centered on two major milestones: Lean proof-backend support and a substantial update to the verified CDCL SAT solver example.
All releases
7 ReleasesStable
QCP-v2.0.4b
QCP-v2.0.4b
QCP v2.0.4b is a maintenance release for the v2.0.4 line. It focuses on bug fixes, a broader example set, improvements to the LLM-assisted proof workflow, and a refreshed QIDE extension.
Stable
QCP-v2.0.4
QCP-v2.0.4
We are pleased to announce QCP v2.0.4. This release expands the C programs that QCP can verify and makes complex verification failures substantially easier to diagnose. It introduces a more complete C preprocessor, floating-point verification, pointer-offset reasoning, reusabl...
Stable
QCP-v2.0.3
QCP-v2.0.3
We are excited to announce the release of QCP v2.0.3! This update focuses on improving AI-assisted proof migration, expanding the verified example suite, refreshing the cross-platform verification toolchain, and adding new libraries for symbolic execution and formal reasoning.
Stable
QCP-v2.0.2
QCP2.0.2
We are excited to announce the release of QCP v2.0.2! This update focuses on enhancing LLM‑driven QCP verification workflows, expanding symbolic execution capabilities, and adding new supporting libraries to simplify verification tasks.
Pre-release
QCP-v2.0beta
v2.0beta
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 autonom...
Stable
QCP-v1.0
v1.0
This is the first release version of Qualified-C-Programming (QCP). QCP is a C program verification tool. Given an annotated C program as input, QCP performs symbolic execution and generates verification conditions to be verified in Rocq.