CryptoProver 实现加密库形式化验证
先了解这件事
2026年10月19日，arXiv发布论文介绍CryptoProver系统。该系统基于AI，能在11.4小时内为curve25519-dalek生成独立证明，并验证RustCrypto中ChaCha20实现符合RFC 8439规范。其特点是从高层API合约自动合成规格与经Verus检查的证明，无需修改可执行代码即可验证生产级密码库。报道提及原开发者曾投入五个月三人 effort 才完成相关工作。
AI 根据报道生成 · 3 小时前更新
报道时间线
沿着报道，了解事件的不同侧面。
- arXiv cs.CRCryptoProver 用 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 流程，可能改变软件供应链安全审计模式，但这需要进一步实证其泛化能力和长期维护成本。
本事件热度走势
当前热度 9·可比范围峰值 9（10月19日 14:00）·近 24 小时可比范围变化 –
趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。