QuickProof：会写单元测试就能形式化验证 C 代码，AI 写证明 Rocq 校验
thomasahle · x · 2026-11-04
形式化验证长期以来因两大门槛让多数开发者望而却步：规格必须用 Lean/Rocq(Coq) 等证明助手语言书写，且证明往往比代码长几倍。GenProof 团队发布 QuickProof，宣称现在只要会写单元测试就能对代码做形式化验证。
- 证明变便宜了：AI agent 现在可以写出完整的形式化证明，证明检查器逐步校验，错误证明无法蒙混过关。
- 规格仍是难点：agent 若找不到原命题的证明，可能悄悄弱化定理或附加假设——读不懂证明语言就发现不了。QuickProof 针对 C 语言解决这一问题：用 C 本身写规格（一个小程序调用被测库，形如属性测试，配合 nondet 不确定输入与 qpassert 断言），工具将其转为定理，AI 证明、Rocq 校验，无需信任 agent 的任何输出。
博文以压缩/解压 round-trip 性质为例演示了完整流程，并称同样的方法甚至能在「已被验证过」的库里找 bug。
「编程与Agent」频道最新
- 开发者反思：让 AI agent 优化 Rust 代码为何比 Go 更难 — unixterminal · 2026-11-04
- 阿里 SPAR 销售智能体实测：20 万商家转化率提升 15.8% — ycombinator · 2026-11-04
- 2637 条提示词、125 亿 token:设计师公开 AI 建站全流程 — tomjohndesign · 2026-11-04
- DeepSeek 长文提出超级智能体架构：连续、高效、主动、持久四大特征 — LangChain · 2026-11-04
- Salesforce 700 人 AI 团队自发从 Cursor 转向 Claude Code — aakashgupta · 2026-11-04
- AI 录屏工具 Wrap 开放内测：Agent 依据操作日志自动剪辑 — therealdanvega · 2026-11-04