QCP v2.1.3 fixes bugs in symbolic execution and Coq/Lean goal generation, and marks QCP's support for the first online preliminary round of the Second Theorem Proving Competition.
What's New
Supporting the Second Theorem Proving Competition
QCP supported the first online preliminary round of the competition's Human–AI Collaboration track, held on September 20, 2026. Participants used QCP or CStar with AI assistance to solve five program verification problems during a two-hour contest.
Across the two platforms, 29 participants submitted solutions, and 10 completed all five problems. Congratulations to all participants!
The second online preliminary round is scheduled for October 10, 2026. We welcome everyone interested in AI-assisted program verification to participate.
For results and participation details, see the competition report.
Bug Fixes
- Fixed bugs in floating-point conversions, empty
forloops, and negative constants. - Fixed predicate renaming in the Coq and Lean goal printers.
- Fixed record-array field readback and preserved symbolic index matching.
Improvements
- Updated the QCP binaries for Windows, Linux, macOS arm64, and macOS x86-64.
- Refreshed generated Rocq verification conditions and proofs for affected examples.
Happy verifying with QCP v2.1.3!