GenProof 发布 QuickProof：用 C 写规格并由 AI 生成 Rocq 证明

GenProof 发布 QuickProof，让开发者用 C 语言编写规格，由 AI 智能体生成形式化证明并交由 Rocq 校验。规格通过 nondet 不确定输入和 qpassert 断言表达，工具将其转为定理，错误证明无法通过检查；原文也提醒，智能体找不到证明时可能弱化定理或附加假设。团队以压缩与解压的 round-trip 性质演示了完整流程，并称该方法还能在已被验证的库中发现 bug。