发表机构
Stanford University; University of North Carolina at Chapel Hill; VMware Research by Broadcom; Amherst College（斯坦福大学; 北卡罗来纳大学教堂山分校; 博通旗下VMware研究院; 阿默斯特学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出基于AI的CryptoProver系统，可从API合约合成内部规范与Verus验证的证明，成功验证了支撑Signal等系统的curve25519-dalek和RustCrypto的chacha20实现，遵循信任优先设计原则。
AI 中文摘要
密码代码是必须正确的关键基础设施，但对生产级库进行形式化验证仍存在困难。现有的语言模型证明系统仅能利用已给定的规范和前提解决孤立的证明义务，尚未解决生产级库的验证问题。本文提出CryptoProver，一种基于人工智能的系统，可从高层API合约合成内部规范及经Verus验证的证明。在不修改可执行代码的前提下，CryptoProver为curve25519-dalek构建了新的独立证明，并根据RFC 8439规范验证了RustCrypto此前未经验证的chacha20实现。这些密码体系支撑着包括Signal和Shadowsocks在内的已部署系统；Signal在全球估计有2.18亿次下载。由人类主导的独立curve25519-dalek验证工作，由5位主要贡献者在8个月内公开完成。在给定API合约以及固定的可信字段规范、算术事实、公理和vstd库的条件下，CryptoProver合成内部规范和证明耗时11.4小时，API记录成本为466.99美元。CryptoProver遵循信任优先的设计原则：机械机制会拒绝规范弱化、自创公理及跨模块破坏，同时隔离机制会阻止参考证明检索，包括从git历史中检索。
英文摘要
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 independent, human-led curve25519-dalek verification was developed publicly over eight months by five main contributors. 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.
