**AI驱动CryptoProver：自动化验证生产级密码库**

_An AI Approach to Verified Production Cryptographic Libraries_

> 研究团队提出CryptoProver，一种基于AI的密码库验证系统，可从高级API契约自动合成内部规范与形式化证明。该系统在11.4小时内、花费466.99美元完成了curve25519-dalek和RustCrypto的chacha20实现的独立验证，而人工验证前者耗时8个月。CryptoProver采用信任优先设计，可机械性拦截规范弱化、发明公理等风险，为Signal等部署系统提供安全保障。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：论文
- **发布时间**：2026-08-05 14:07（北京时间）
- **原文**：[打开原文](https://arxiv.org/abs/2608.00965)