CryptoProver 用 AI 在 11.4 小时内生成曲线25519-dalek的独立证明并验证ChaCha20实现

这篇论文提出 CryptoProver，一个基于 AI 的系统，能从高层 API 合约自动合成内部规格和经 Verus 检查的证明，无需修改可执行代码即可验证生产级密码库。该系统成功为 curve25519-dalek 构建了新的独立证明，并验证了 RustCrypto 中此前未经验证的 chacha20 实现是否符合 RFC 8439 规范。

关键事实显示，原开发者曾投入五个月三人 effort 才完成 curve25519-dalek 的验证，而 CryptoProver 在给定 API 合约和固定可信库（含域规格、算术事实、公理及 vstd）的条件下，仅用 11.4 小时和 466.99 美元 API 成本即完成同等任务。系统遵循信任优先设计，通过机械门控拒绝规格弱化、发明公理和跨模块破坏，并通过隔离机制阻断从 git 历史等来源检索参考证明。

推断：该成果表明 AI 辅助形式化验证可能显著降低高安全需求基础设施的验证门槛，但当前仍依赖特定领域知识库和严格约束。猜测：若此类工具能扩展至更多密码原语或集成到 CI/CD 流程，可能改变软件供应链安全审计模式，但这需要进一步实证其泛化能力和长期维护成本。