QCP简介
QCP（Qualified C Programming）是一个 C 程序验证工具。其核心功能是要让用户可以验证并确认一个 C 语言能在所有允许的情况下都安全运行且行为符合预期。使用 QCP 时，用户需要为 C 代码添加规约标注 （如函数的前后置条件、循环不变量等），之后 QCP 会通过符号执行和分离逻辑推理，将程序的安全性及功能 正确性验证转化为一组验证条件（Verification Conditions, VC）。对于大多数简单 VC，QCP 会使用内置 求解器完成验证。对于无法自动求解的部分，QCP 会生成 Rocq（原 Coq）证明文件，用户可在定理证明器中 手动补全证明作为兜底方案。
不同于传统的程序验证工具，QCP 提供了专门的 IDE 套件，用户可以通过 VSCode 插件或者 QCP 网页版使用。在 QCP 的 IDE 支持下，用户在编写程序的同时，可以随时查看当前程序状态所满足的断言（也就是符号执行的中间结果）， 不需要编写完整个函数即可进行验证，在编写过程中支持随时查看符号执行结果，第一时间检查断言标注的合理性， 修正其中的错误。
QCP 2.0 Beta 版在之前的基础上，还提供了 AI 协作验证的支持。现在，用户可以在 AI 的协助完成标注添加 和 Rocq 证明补全。QCP 2.0 让验证更加智能化、自动化！
