Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt
Authors: Yupeng Ren, Zhaoxuan Li, Rui Zhang
Organizations: State Key Laboratory of Cyberspace Security Defense, Institute of Information Engineering, Chinese Academy of Sciences, Beijing 100085, China · School of Cyber Security, University of Chinese Academy of Sciences, Beijing 100049, China
Large language models (LLMs) have recently made substantial progress in formal proof generation, yet presenting distinctive challenges in cryptographic area. Computational security arguments posit that a valid proof must coordinate probability, adversarial games, invariants, assumptions and bounds, which can be provided by a machine-checked framework named EasyCrypt. Although all objects may appear in available context, LLMs still struggle because proof-theoretic dependencies are typically implicit in a linear representation and distributed across multiple programs. So, this paper presents Scratchy, a visual-scratchpad approach that exposes these dependencies for multimodal generation. Given the natural-language security description, with formal context and target propositions, the proof objects can be normalized into a typed proof-relation graph. Then a structure-preserving visual compiler transforms the graph into the formula-rich visual proof state that guides a multimodal model in generating the EasyCrypt proof. Also, the Scratchy-eval, a 114-task dataset derived from reliable official EasyCrypt files, has been introduced. It contains 64 security-form proof generations and 50 multiple-choice knowledge tests. After a series of evaluations, covering semantic grounding, relational invariants, and game reductions, classical LLMs like GPT-5.6-Sol and Claude-Opus-5 have gained a clear advantage from Scratchy's structured visual proof states. This contrast suggests that explicit proof structure can make the improvement and multimodal proof-state representation as a promising direction for computer-aided cryptography.
Figures & tables
Figure 1: Results of the API-based EasyCrypt proof-generation Observation across six representation conditions. The professional multimodal graph achieves the highest compile pass rate (62.5%, 25/40), outperforming all baselines.
Symbol
Meaning
X,x
Security setting and task.
C,Γ
Local context and environment.
ϕ
Target obligation.
q
Structured Natural-Language Proof Sketch.
G=(V,E,τ,λ)
Typed relation graph.
V,E
Graph nodes and edges.
Table 1: Notation expolited in the Scratchy pipeline and the motivating Observation.
Figure 2: Complementary views of the Observation. The gray curve is the observed reference profile, and the rose curve is a comparison profile anchored to it. Models involve Claude-opus-5, Gemini-3.7-flash, Kimi-k3, GPT-5.6-sol and Gemma-4-26B-A4B.
ID
Focus
Proof object
Official source
01
Semantic
Well-foundedness
WF-examp.ec
02
Semantic
Dice point mass
Dice4_6.ec
03
Semantic
While termination
WhileSampling.ec
04
Relational
Async invariant
async-while.ec
05
Relational
Bad-event split
FundamentalLemma.ec
06
Reduction
Pedersen hiding
Pedersen.ec
Table 2: Sources of the ten paired Observation samples. All files are drawn from the pinned official EasyCrypt repository snapshot EasyCrypt Development Team (2026) .
Figure 3: The Scratchy pipeline. Structured proof context and an SNPS are deterministically compiled into a typed proof-relation graph and a formula-rich visual scratchpad. A multimodal model follows the explicit dependencies to synthesize an EasyCrypt proof fragment, which is reconstructed and checked for acceptance or an open outcome.
Figure 4: Professional visual proof state for a PIR relational obligation. The graph organizes source facts, the target, a proof-rule route, and the machine-checkable goal into a directed path.
Table 3: Scratchy-eval results under six representation conditions. Each numeric entry is passed/total (%). NR: no relation knowledge; TH: theorem-only text; CR: coarse proof-relation text; GD: generic diagram; SG: shuffled-edge graph; PG: Scratchy professional graph.
Figure 5: Generation pass rates across seven source families, pooled over four models. Each vertical group compares CR (coarse proof-relation text), SG (shuffled-edge graph), and PG (Scratchy professional graph); bar height and top labels report the percentage of fragments accepted by EasyCrypt. PG leads on the four cryptography and reduction-oriented families, SG leads on foundations and program analysis, and the two graph conditions tie on program logics.
Table 5: Category-level coverage of Scratchy-eval. Representative material and proof emphasis are summarized without enumerating task IDs or hidden fragments. The generation counts sum to 64; static-validity and semantic-recognition diagnostics accompany all seven families.
The large language models (LLMs) might produce a persuasive argument within mathematical and logical fields, although such argument often includes some minor missteps, including the entire omission of side conditions, invalid inference patterns, or appeals to a lemma that cannot be derived logically out of the context being discussed. These omissions are infamously hard to notice solely out of the text, as even the misconstrued construction still may seem mostly accurate. Conversely, interactive theorem provers like Lean and Coq have rigorous reliability by ensuring that syntactic and semantic statements only accept statements that can pass all the syntactic and semantic steps in the program which is a small trusted kernel of the language type-checks with. Despite the fact that this technique provides strong guarantees, it comes at quite a heavy price: the evidence must be completely formalized, and the evidence user or a auxiliary search program must provide an avalanche of low-level information. This paper presents a hybrid pipeline where an LLM generates a typed proof sketch in a compact DSL and a lightweight trusted kernel expands the sketch into explicit proof obligations.
Kranthi Kommuru, Kunal Khanvilkar, Gaurav Parekh
Automatic Data Processing, Inc Atlanta, USA · Amazon Web Services, Inc Banglore, India
Neurosymbolic approaches leveraging Large Language Models (LLMs) with formal methods have recently achieved strong results on mathematics-oriented theorem-proving benchmarks. However, success on competition-style mathematics does not by itself demonstrate the ability to construct proofs about real-world implementations. We address this gap with a benchmark derived from an industrial cryptographic library whose assembly routines are already verified in HOL Light. s2n-bignum is a library used at AWS for providing fast assembly routines for cryptography, and its correctness is established by formal verification. The task of formally verifying this library has been a significant achievement for the Automated Reasoning Group. It involved two tasks: (1) precisely specifying the correct behavior of a program as a mathematical proposition, and (2) proving that the proposition is correct. In the case of s2n-bignum, both tasks were carried out by human experts. In s2n-bignum-bench, we provide the formal specification and ask the LLM to generate a proof script that is accepted by HOL Light within a fixed proof-check timeout. To our knowledge, s2n-bignum-bench is the first public benchmark focused on machine-checkable proof synthesis for industrial low-level cryptographic assembly routines in HOL Light. This benchmark provides a challenging and practically relevant testbed for evaluating LLM-based theorem proving beyond competition mathematics. The code to set up and use the benchmark is available here: s2n-bignum-bench.
Balaji Rao, John Harrison, Soonho Kong +2
Stevens Institute of Technology Hoboken, NJ 07030 · Amazon Web Services Seattle, WA 98101
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.
Chuyue Sun, Su Fong, Zhiyi Kuang +5
Stanford University · &Truth · University of North Carolina at Chapel Hill +2