ShannonProver: Towards Automating Formal Cryptographic Proofs
ShannonProver is an agentic framework that automates cryptographic proofs by creating scripts for proof assistants from a high-level security model and lemma decomposition. It uses state-aware context management and multi-agent orchestration to guide agents through the proof process, significantly reducing errors and improving solution rates for complex lemmas.