ShannonProver: Towards Automating Formal Cryptographic Proofs
Cryptographic proofs are produced at a scale that increasingly exceeds the community's ability to verify them manually. Machine-checked proofs offer a path toward scalable proof verification, but they shift the bottleneck to writing the proofs themselves: even when the high-level proof plan is known, turning it into a proof script requires spelling out every detail the plan leaves implicit, which is laborious even for experts. This paper presents ShannonProver, an agentic system for automating cryptographic proofs. Given a protocol and its security definitions modeled by a cryptographer, ShannonProver decomposes the main theorem into intermediate games and lemmas, and constructs EasyCrypt proof scripts for those lemmas. We evaluate ShannonProver on a new dataset of lemmas in EasyCrypt. The benchmark spans textbook primitives, deployed standardized protocols, as well as recent NIST proposals, and includes expert case studies drawn from a corpus that has not previously been available online. On case studies such as ChaChaPoly1305 and MEE-CBC, ShannonProver completes within hours proof developments that historically took experts weeks to months. More broadly, this work suggests a path toward accelerating cryptographic research: as agents automate the proof-engineering burden, cryptographers can iterate more quickly on new constructions, obtain machine-checked assurance earlier, and bring protocols from design to deployment faster.