Preprint
Aug 2026
An AI Approach to Verified Production Cryptographic Libraries
An AI-based system that synthesizes internal specifications and Verus-checked proofs from high-level API contracts, CryptoProver, which constructs a new independent proof of curve25519-dalek and verifies RustCrypto's previously unverified chacha20 implementation against an RFC 8439 specification.
Chu-Yue Sun, S. Fong, Zhi-Yi Kuang et al.
· 0 citations