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.

Read full release notes →

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.

Read full release notes →

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...

Read full release notes →

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.

Read full release notes →

QCP-v2.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.

Read full release notes →

QCP-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...

Read full release notes →

QCP-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.

Read full release notes →