arXiv cs.AI· Chuyue Sun, Su Fong, Zhiyi Kuang, Yizheng Jiao, Nina Narodytska, Haoze Wu, David L. Dill, Clark Barrett·· 12 小时前AI 评分58
CryptoProver：从 API 契约自动合成密码库验证证明
An AI Approach to Verified Production Cryptographic Libraries
AI 导读
研究团队提出 CryptoProver，可从高层 API 契约自动合成内部规格与经 Verus 检查的证明，在不改动可执行代码的前提下为 curve25519-dalek 构建独立证明，并依据 RFC 8439 规格验证 RustCrypto 此前未验证的 chacha20 实现。
正文 · 原文
Abstract:Cryptographic code is critical infrastructure that must be correct, yet formally verifying production libraries remains difficult. Existing language-model proof systems solve isolated obligations with specifications and premises already given, leaving production-library verification unresolved.
We present CryptoProver, an AI-based system that synthesizes internal specifications and Verus-checked proofs from high-level API contracts. Without changing executable code, CryptoProver constructs a new independent proof of curve25519-dalek and verifies RustCrypto's previously unverified chacha20 implementation against an RFC 8439 specification. These cryptographic lineages underpin deployed systems including Signal and Shadowsocks; Signal has an estimated 218M global downloads. The original developers report a focused five-month, three-person effort to verify curve25519-dalek. Given the API contracts and a fixed trusted library of field specifications, arithmetic facts, axioms, and vstd, CryptoProver synthesizes the internal specifications and proofs in 11.4 hours with USD 466.99 in recorded API cost. CryptoProver follows a trust-first design principle: mechanical gates reject specification weakening, invented axioms, and cross-module breakage, while isolation blocks reference proof retrieval, including from git history.
| Subjects: | Cryptography and Security (cs.CR); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2608.00965 [cs.CR] |
| (or arXiv:2608.00965v2 [cs.CR] for this version) | |
| https://doi.org/10.48550/arXiv.2608.00965 arXiv-issued DOI via DataCite |
Submission history
From: Chuyue Sun [view email]
[v1]
Sun, 2 Aug 2026 03:32:08 UTC (146 KB)
[v2]
Fri, 16 Oct 2026 09:00:33 UTC (154 KB)
来源：arXiv cs.AI · arxiv.org