Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis

Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis Shichen Huang∗ , Zhenghe Jiang∗ , Yi Jiang† , Ling-I Wu‡ , Jingyang Li‡ Guoqiang Li‡ B ∗ Shanghai Polytechnic University † Nanjing University of Science and Technology

arXiv:2607.19795v1 [cs.SE] 22 Jul 2026

‡ Shanghai Jiao Tong University

Abstract—Zero-Knowledge Ethereum Virtual Machines (zkEVMs) secure Ethereum rollups by generating zeroknowledge proofs that guarantee off-chain execution correctness. However, subtle implementation bugs (e.g., incorrect gas accounting) can lead to valid proofs certifying semantically faulty states, thereby silently defeating cryptographic guarantees. Formal verification via SMT solvers can prevent this, but is bottlenecked by specification: current zkEVM development practice lacks automated methods to translate Rust opcode handlers into verification models. Current practices rely on unsustainable manual specifications, while LLM-based approaches suffer from hallucination and lack formal guarantees. To address this, we propose VeriSynth, a framework that synthesizes executable Python/Z3 verification models from Rust zkEVM code. VeriSynth enforces a hybrid paradigm: an LLM acts strictly as a formalization frontend to translate code into symbolic constraints, while an SMT solver serves as the correctness arbiter. To handle complex multi-component state transitions, VeriSynth integrates semantic decomposition, retrieval-grounded prompting, and verification-guided autorepair into a closed-loop pipeline. We evaluate VeriSynth on the first source-level zkEVM verification benchmark, encompassing both correct and faulty opcode implementations. VeriSynth achieves a bug detection rate of over 90%, substantially outperforming direct and conversational LLM baselines, as well as a production-grade handwritten mutation-testing suite. Ablation studies confirm that each pipeline component is critical to the framework’s overall effectiveness. Index Terms—formal verification, specification inference, constraint synthesis, large language models, SMT solving, zkEVM

I. I NTRODUCTION The massive growth of decentralized software systems has led Ethereum to increasingly offload execution to Layer2 infrastructures called rollups, which scale throughput by processing transactions off-chain [1]. To ensure the integrity of these decoupled states, the underlying blockchain employs a Zero-Knowledge Ethereum Virtual Machine (zkEVM) to construct mathematical validity proofs that verify off-chain transitions [2]. However, this verification pipeline relies on a fundamental software engineering assumption: the zkEVM implementation must faithfully realize the intended virtual machine semantics. If this implementation contains subtle bugs—such as incorrect gas accounting, missing state updates, or wrong boundary checks—the system can generate valid cryptographic proofs for semantically faulty execution states. These silent semantic errors bypass proof verification, creating

a critical need for automated, solver-backed formal verification of the source-level zkEVM code [3]–[6]. Addressing this challenge involves two distinct layers: automated reasoning and verification model synthesis. At the reasoning layer, modern SMT solvers and symbolic reasoning engines already provide mature backends for checking logical constraints over bit-vectors, arrays, and state-transition relations [7]–[10]. At the synthesis layer, however, the situation is different: solvers can only reason about the constraints they are given; they do not automatically infer specifications or verification conditions from an implementation [11]–[13]. This semantic gap is especially pronounced in zkEVM implementations, where complex execution behaviors are implicit in lowlevel Rust source code. Consequently, the central bottleneck in zkEVM verification is not the capability of the reasoning backend, but the lack of automated, practical tooling for translating implicit, source-level Rust semantics into accurate, solver-ready verification models at the opcode level. Current software engineering workflows do not close this synthesis gap, because they leave the constraint-modeling burden on human developers. Leading zkEVM projects such as Scroll rely on manually written specifications and handcrafted mutation tests to detect semantic bugs [14]. However, maintaining these manual artifacts does not scale as lowlevel implementations undergo frequent optimization, and tests are bounded by the behaviors that developers explicitly anticipate. Furthermore, while the community has constructed benchmarks for smart contract and EVM bytecode vulnerabilities [15], there is no standardized, source-level bug benchmark for zkEVM Rust implementations. As a result, developers shoulder the modeling effort, and researchers lack a concrete baseline for evaluating automated verification model synthesis at the infrastructure layer. LLM-based methods offer a potential path to reduce this manual burden, but they are not reliable enough on their own. Existing LLM-based specification generators primarily produce high-level declarative properties [16], [17], whereas verifying zkEVM opcode transitions requires detailed executable models that capture multi-component state updates across stack, memory, storage, gas, and execution context [18], [19]. More critically, direct LLM bug-finding suffers from code hallucination and provides no formal guarantees. To scale verification to complex systems, a hybrid paradigm is needed: the LLM acts strictly as a formalization frontend that translates

Fig. 1. Motivation of LLM-guided verification model synthesis. Existing approaches fail to translate Rust implementations into formal verification models due to implicit semantics and complex opcode behaviors. Our approach bridges this gap by synthesizing executable SMT constraints that can be directly validated by a solver.

code into candidate executable SMT constraints, while an SMT solver serves as the correctness arbiter. No existing automated framework realizes this paradigm for source-level Rust zkEVM implementations.

the detection rate from 91.6% to 66.3%, as many initially generated models fail on local syntax or sort errors rather than semantic misunderstandings. Retrieval grounding and semantic decomposition each provide further gains.

To address these gaps, we introduce VeriSynth, a framework that synthesizes executable Python/Z3 verification models from zkEVM Rust source code. Its core design separates responsibilities: an LLM serves as a formalization frontend that translates source-level code into candidate symbolic constraints, while an SMT solver acts as the correctness arbiter: the LLM proposes, the solver decides. VeriSynth targets the full zkEVM execution state, guiding the LLM to extract semantics that are otherwise implicit in Rust control flow and encoding them as symbolic variables and constraints covering stack manipulations, memory layouts, persistent storage updates, dynamic gas and refund accounting, and execution context registers. To make these interacting components tractable, the framework integrates three mechanisms into a closedloop pipeline: semantic decomposition isolates state transitions into modular verification units; retrieval-grounded prompting anchors variable types and solver APIs against previously validated examples; and verification-guided auto-repair iteratively refines generated models using compiler diagnostics and solver counterexamples until they compile and verify.

To demonstrate practical engineering value, we compare VeriSynth directly with Scroll’s handwritten Rust mutationtest workflow. Scroll’s production-grade tests expose 55 out of 95 injected bugs, while VeriSynth detects 87—32 additional bugs that escaped manually written assertions. This gap is consistent across both semantic errors and execution-path errors, indicating that automated constraint synthesis complements, rather than replaces, manual testing pipelines.

We evaluate VeriSynth on our self-constructed source-level zkEVM verification benchmark of 95 injected faulty samples across five opcode semantic families. VeriSynth detects 87 out of 95 bugs, achieving a detection rate of 91.6%, substantially outperforming the LLM-only baseline (46.3%) and the conversational LLM baseline (61.1%). The framework remains effective across diverse opcode families, with perfamily detection rates ranging from 95.5% (arithmetic/bitwise) to 85.7% (call/create paths). Ablation confirms that autorepair is the single largest contributor: removing it drops

The main contributions of this paper are as follows: We propose VeriSynth, an LLM-guided verification framework that synthesizes executable Python/Z3 models directly from zkEVM Rust source. VeriSynth treats LLMs as formalization frontends and SMT solvers as final validators, integrating semantic decomposition, retrievalgrounded prompting, and verification-guided auto-repair into a closed-loop pipeline. • We construct the first source-level benchmark for Rust opcode implementation verification in zkEVM systems, spanning five semantic families of injection faults in control flow, state updates, and resource accounting. This benchmark targets implementation-level faults, a category distinct from existing contract- and bytecode-level datasets. • We conduct a systematic empirical evaluation showing VeriSynth substantially outperforms direct LLM baselines and industrial mutation-testing workflows. Ablation studies confirm that auto-repair and retrieval grounding are critical for solver compatibility and model executability. •

II. PRELIMINARY A. Zero-Knowledge Ethereum Virtual Machines A zero-knowledge Ethereum Virtual Machine (zkEVM) executes Ethereum-compatible programs and generates zeroknowledge proofs showing that the resulting state transitions satisfy a predefined constraint system. In rollup systems, transactions are executed off-chain, while the corresponding proofs are verified on-chain, allowing a large batch of executions to be validated without re-executing every instruction. An EVM execution state can be abstracted as

under which the implementation violates the property. If it is unsatisfiable, the property holds for all executions captured by the encoded model and its assumptions. Although SMT solvers provide reliable reasoning backends, they require explicit, complete, and correctly typed constraints. Constructing such verification models from low-level source code therefore remains a major bottleneck. VeriSynth addresses this problem by using an LLM to synthesize executable Python/Z3 models while retaining the SMT solver as the final correctness arbiter.

σ = ⟨pc, stk, mem, sto, gas, env⟩,

Large language models (LLMs) have demonstrated strong capabilities in source-code understanding, generation, and program repair [18], [21], [22]. Through pretraining on large code corpora and in-context learning, LLMs can infer relationships between variables, control-flow branches, function calls, and state updates. These capabilities make them useful for translating implementation-level program behavior into executable verification scripts. Recent studies have explored LLMs for formal specification generation, property inference, and feedback-driven program repair [16], [17], [23]. Nevertheless, generating an executable verification model is more demanding than producing a natural-language explanation or a high-level property. The model must correctly represent path conditions, symbolic types, state updates, resource accounting, and solver-specific APIs. Small mistakes, such as using inconsistent bit-vector widths or omitting a branch condition, can make the generated model either non-executable or semantically unsound. Therefore, LLM-generated artifacts cannot provide formal correctness guarantees by themselves. VeriSynth uses the LLM only as a formalization frontend that translates zkEVM source code into candidate Python/Z3 models. Compilation diagnostics, type and sort errors, solver exceptions, and counterexamples are then used as structured feedback to repair incomplete or inconsistent models. The LLM proposes the symbolic model, while the SMT solver determines whether the encoded correctness properties hold.

where pc denotes the program counter, stk the operand stack, mem the transient memory, sto the persistent storage, gas the remaining gas, and env the execution context. Each opcode o defines a transition relation To (σ, σ ′ ), which specifies how a valid pre-state σ is transformed into a post-state σ ′ according to the EVM semantics [2], [6]. Depending on the opcode, the transition may involve 256bit arithmetic, stack manipulation, memory expansion, storage modification, gas accounting, or exceptional control flow. A valid zero-knowledge proof guarantees that a witness satisfies the constraints encoded in the proving circuit. However, it does not independently guarantee that the sourcelevel executor or witness generator faithfully implements the intended EVM semantics. Bugs such as incorrect gas charging, missing state updates, improper boundary checks, or faulty control-flow handling may therefore produce valid proofs for semantically incorrect state transitions [20]. This work focuses on verifying such implementation-level opcode semantics before they are incorporated into the proving process. B. Formal Verification Formal verification establishes program correctness by expressing implementation behavior and required properties as mathematical constraints. Symbolic execution replaces concrete inputs with symbolic variables and accumulates path conditions and state-transition constraints, thereby representing multiple program executions within a single logical model [11]. This approach is particularly suitable for opcode implementations whose behavior depends on stack values, storage contents, gas conditions, and execution branches. Satisfiability Modulo Theories (SMT) solvers support logical theories such as fixed-width bit-vectors, integers, arrays, and uninterpreted functions. These theories naturally model EVM word arithmetic, memory and storage structures, conditional transitions, and resource constraints [7], [8]. Let CP (σ, σ ′ ) encode the behavior of an implementation P , and let Φ(σ, σ ′ ) denote an intended semantic or safety property. Verification checks the satisfiability of CP (σ, σ ′ ) ∧ ¬Φ(σ, σ ′ ). If the formula is satisfiable, the solver returns a model that serves as a counterexample, demonstrating an execution

C. Large Language Models

III. A PPROACH This section presents VeriSynth, an LLM-guided framework for synthesizing executable verification models from sourcelevel implementations. The key design principle is to use LLMs for semantic model construction while leaving correctness checking to an SMT solver. Given an input implementation, VeriSynth decomposes the program into verificationrelevant semantic units, retrieves previously validated examples as semantic anchors, synthesizes executable SMT constraints, and repairs failed models using compiler and solver feedback. Following the generate-and-verify paradigm used in recent LLM-assisted specification generation and repair work [16], [23], VeriSynth adopts an iterative workflow in which candidate verification models are generated, checked, and refined. However, unlike approaches that generate declarative specifications such as JML annotations, VeriSynth generates

executable verification models that can be directly checked by Z3. This distinction is important for zkEVM implementations, where execution semantics such as opcode dispatch, storage updates, gas accounting, and environment-dependent behavior are often implicit in source code rather than written as formal specifications. A. Overview and Problem Formulation The input of VeriSynth is a source program P written in a supported language. The language-specific front end parses P and normalizes it into an intermediate representation from which verification-relevant semantic units are extracted. A semantic unit may correspond to an opcode handler, a state transition routine, a memory or storage update, or a helper function that participates in execution semantics. In the zkEVM context, we classify units into five semantic families: arithmetic/bitwise, memory/storage, gas/refund, call/create paths, and environment/context-dependent behavior. For each semantic unit u, VeriSynth aims to synthesize an executable verification model: Mu = ⟨Vu , Cu , Φu ⟩,

(1)

where Vu is the set of symbolic variables, Cu is the set of solver constraints encoding the behavior of u, and Φu is the property or consistency obligation to be checked. The symbolic state of zkEVM-style code typically contains stack, memory, storage, gas, refund, warm-access information, and environment variables, following the stateful execution model of the EVM [2], [6]. The generated constraints describe how such a state is transformed by the target unit. The verification task is to check whether the synthesized model admits a counterexample under the chosen abstraction. Given the model in Eq. 1, if Cu ∧ ¬Φu is unsatisfiable, the model is accepted with respect to Φu ; otherwise, the solverproduced counterexample is treated as feedback for repair, indicating a potential semantic inconsistency in the original implementation. This formulation makes the goal of VeriSynth different from test generation or natural-language explanation. The framework does not ask the LLM to decide whether a program is correct. Instead, the LLM proposes an executable model, and the solver validates whether the proposed model satisfies the intended constraints. VeriSynth separates the model extracted from the target implementation from the obligations used to evaluate it. For a semantic unit u, Cuimpl (σ, σ ′ ) encodes the behavior of the source implementation, while Φu is constructed from validated opcode semantics and family-specific consistency rules rather than from the target code alone. The verification query is Cuimpl (σ, σ ′ ) ∧ ¬Φu (σ, σ ′ ).

(2)

Typical obligations include arithmetic equivalence, stackheight preservation, storage-update consistency, gas and refund bounds, and correct failure or return-value propagation. A satisfiable query yields an input state under which the implementation violates the expected behavior. This separation

prevents an incorrect but internally consistent implementation model from being accepted solely because the generated constraints reproduce the same faulty logic. B. Semantic Decomposition and Retrieval The formulation above assumes a semantic unit u is already isolated. In practice, raw zkEVM source files intermix opcode handlers, helper routines, and state objects. Directly applying LLMs to such files is unreliable because the relevant semantics are scattered across these components. Therefore, VeriSynth first decomposes the input into semantically coherent units. The purpose of decomposition is not merely to reduce prompt length, but to expose state effects that can be modeled independently while preserving explicit dependencies through unit interfaces. For each code fragment, VeriSynth identifies which state components it reads and writes, and assigns it to a semantic family. Fragments contributing to the same state transition are grouped into one unit. For example, an SSTORE-like unit may include reading the current storage value, detecting the noop case, updating the warm-access state, computing gas cost, and writing the new storage value. Although these operations appear as separate statements in Rust, they jointly define one semantic transition and should be modeled together. Figure 2 illustrates this mapping for an SSTORE unit. Retrieval-augmented prompting has been used to provide LLMs with task-specific context in code and specification generation tasks [17], [19]. In VeriSynth, retrieval is used differently: the retrieved examples serve as semantic anchors for executable model construction. After decomposition, VeriSynth retrieves similar verified examples from a reference database: D = {(ur , M r , metar )}, where ur is a reference unit, M r is its verified executable model, and metar records metadata such as opcode family, state components, and modeling patterns. Given a target unit u and a reference unit d, their similarity is computed as: E MB(u) · E MB(d) + (1 − α) · FAM(u, d), ∥E MB(u)∥∥E MB(d)∥ (3) where E MB(·) denotes the code embedding and FAM(u, d) rewards matches in opcode family or semantic category. Based on this similarity measure (Eq. 3), the top-k examples are used as semantic anchors for synthesis. The retrieved examples are not copied as templates. Instead, they serve as a modeling prior: they stabilize the symbolic vocabulary, state schema, and transition structure by grounding generation in previously validated modeling decisions. Each reference entry is added to the retrieval database only after its executable model passes syntax checking, sort checking, solver execution, and the associated semantic obligations. During retrieval, VeriSynth prioritizes examples with compatible opcode families, accessed state components, and symbolic types. The retrieved models guide symbolic declarations, transition S IM(u, d) = α ·

Fig. 2. Example of semantic-to-SMT synthesis. Given a Rust implementation of the SSTORE opcode, VeriSynth maps key semantic operations to precise state-transition constraints and safety properties, producing an executable verification model ready for SMT solving.

structures, and solver usage rather than being directly copied. To prevent evaluation leakage, examples sharing the same source-file identity or opcode unit with the target are excluded from the candidate set.

no op := (cur = val),

C. LLM-Guided Constraint Synthesis VeriSynth uses a typed symbolic state shared across generated models. EVM words are represented as fixed-width bitvectors, control flags as Boolean expressions, and memory and storage as symbolic arrays. The state is divided into pre-state and post-state variables: σ = ⟨stk, mem, sto, gas, ref, ctx, status⟩, σ ′ = ⟨stk ′ , mem′ , sto′ , gas′ , ref ′ , ctx′ , status′ ⟩.

constraints such as gas and refund behavior, and assertions or safety obligations. To illustrate the intended mapping from code to constraints, consider a simplified SSTORE unit (illustrative example): warm′ := true, gas cost := ite(no op, 0, sstore cost(cur, val)), gas′ := gas − gas cost, store′ := ite(no op, cur, val). The corresponding safety obligations can be written as:

(4)

Source-level branches are translated into guarded constraints or Z3 If expressions, while Rust assignments define equalities over post-state variables. Each state component must either be explicitly updated or connected to its pre-state through a frame condition. For example, an opcode that does not modify memory introduces mem′ = mem. These frame conditions prevent omitted updates from leaving post-state variables unconstrained. The encoding also enforces consistent bit-vector widths and explicit status variables for exceptional exits, reducing ambiguity during constraint synthesis and providing structured targets for solver-guided repair. LLMs have shown strong capabilities in code generation and code understanding [21], [24]. In VeriSynth, we use this capability to translate each semantic unit into an executable SMT model rather than a natural-language description. For a target unit u, the prompt contains four parts: the source code of u, the retrieved semantic anchors, opcode-aware modeling instructions, and the required output format. The opcode-aware instructions specify the relevant symbolic state schema (stack, memory, storage, gas, environment variables) and modeling obligations for the semantic family of u, guiding the LLM to encode the appropriate variable types, transition structure, and safety assertions. When repair is needed, compiler diagnostics or solver feedback are additionally appended to the prompt. The synthesized constraint set falls into four categories: guard and path conditions, state-transition constraints, resource

gas′ ≥ 0, no op ⇒ store′ = cur, ¬no op ⇒ store′ = val. D. Executable Verification and Auto-Repair The generated model may still fail verification. Common failures include missing declarations, invalid Python or Z3 API usage, bit-vector sort mismatches, incomplete state updates, or semantic inconsistencies exposed by counterexamples. Instead of discarding failed models, VeriSynth repairs them using structured feedback from the compiler and solver, following the broader idea of feedback-driven LLM repair [23]. cu , the As formalized in Eq. 5, given a candidate model M verifier returns: cu ) = ⟨ok, e, w⟩, V ERIFY(M

(5)

where ok indicates whether the model passes verification, e is the error class, and w is an optional witness such as a compiler trace or solver counterexample. Verification proceeds in four stages. VeriSynth first parses and imports the generated Python script, then constructs the symbolic expressions to detect missing declarations and sort mismatches. Next, it executes the solver query under a bounded timeout and finally checks the semantic obligations. When a stage fails, only the corresponding diagnostic and the relevant model fragment are returned to the LLM, enabling localized repair while preserving constraints that have already passed earlier checks.

TABLE I LLM- GUIDED SYNTHESIS AND REPAIR .

must pass syntax, sort, execution, and semantic checks. Thus, an unsatisfiable query establishes correctness only within the modeled state and assumptions, rather than for the entire zkEVM implementation.

Input

P (source program), D (reference database), R (repair action set), k (retrieval count), Tmax (repair budget).

Output

Verified executable models for all accepted units.

IV. E XPERIMENTAL S ETUP

Procedure

1) Parse and normalize P . 2) Decompose P into semantic units. 3) Initialize Mfinal ← ∅. 4) For each unit u: a) Identify semantic family f (u). b) Retrieve top-k anchors from D. cu . c) Synthesize candidate model M cu . d) Verify M e) If verification fails, repair the model using compiler/solver feedback. f) Repeat until accepted or Tmax is reached.

In this section, we introduce the experimental design, dataset, baselines, and evaluation metrics used to evaluate VeriSynth. Our experiments are organized around the following research questions:

TABLE II E RROR CATEGORIES AND REPAIR ACTIONS IN V ERI S YNTH . Error Parse Sort Execution Semantic

Source Compiler Z3 exception Traceback Counterexample

Repair Action Fix syntax, imports, and missing declarations. Align bit-vector widths and symbolic sorts. Repair invalid APIs and solver construction. Refine guards, transitions, and constraints.

RQ1: Effectiveness. How accurately can VeriSynth detect opcode-related semantic bugs? • RQ2: Opcode-Family Generalization. Does VeriSynth remain effective across different opcode semantic families? • RQ3: Ablation. How much do semantic decomposition, retrieval grounding, opcode-aware prompting, auto-repair, and solver-backed validation contribute to the final performance? • RQ4: Token Cost. What is the token cost of the full verification pipeline? • RQ5: Practical Value. Compared with Scroll’s handwritten Rust mutation-test workflow, what additional bugdetection value does VeriSynth provide? •

We classify repair-relevant failures into four categories: E = {Eparse , Esort , Eexec , Esem }. Here, Eparse denotes syntax or missing-declaration errors, Esort denotes type or sort mismatches, Eexec denotes solver execution failures or timeouts, and Esem denotes semantic inconsistencies exposed by solver witnesses. For each error class e, VeriSynth maintains a candidate repair set R(e). A repair action may complete missing declarations, correct bit-vector widths, replace invalid operators, refine guard constraints, patch state updates, or regenerate a localized fragment of the model. Repair actions are applied in a fixed priority per error class (Table II), favoring actions with minimal structural modification. Table I summarizes the overall procedure. The loop terminates when the model passes all verification phases or the repair budget is exhausted. This bounded process prevents unbounded regeneration and makes the system behavior measurable. Finally, VeriSynth is verification-guided rather than LLMtrusting. The LLM proposes candidate models; the compiler and SMT solver check their executability and internal consistency. This shifts error detection from LLM judgment to machine-checkable consistency. Thus, the framework uses LLMs to reduce the manual burden of formal modeling while retaining solver-backed checking as the final validation mechanism. The guarantees of VeriSynth are relative to the extracted semantic unit, symbolic abstraction, and encoded obligations. The LLM is not treated as a correctness oracle; its output

A. Implementation We implement VeriSynth as a prototype framework that integrates language-specific front ends, retrieval-guided prompting, executable Python/Z3 model synthesis, and verificationguided repair. The current prototype supports source-level analysis of Rust programs and generates Python/Z3 verification scripts. For each target program, VeriSynth first extracts verification-relevant semantic units, retrieves similar verified examples from a reference database, generates executable SMT models, and invokes Z3 to check the synthesized constraints. We use GPT-4o as the backend LLM in the current evaluation. The maximum number of repair iterations is set to 3. For each sample, we record the final detection result, executability status, repair behavior, and token usage. Since the current prototype is intended for offline verification of security-critical implementation logic, our cost analysis focuses on token consumption rather than online runtime overhead. B. Dataset We evaluate VeriSynth on a self-constructed benchmark of 95 negative samples derived from zkEVM-style opcode implementation logic. Each sample contains one localized opcode-related bug injected into a target semantic unit while preserving most of the surrounding code structure. The benchmark is designed to evaluate whether VeriSynth can detect semantic inconsistencies in implementation-level opcode logic.

1) Negative-sample Construction: To construct the benchmark, we inject one bug into each target unit. The injected errors include wrong arithmetic rules, incorrect boundary handling, missing state updates, wrong return-value propagation, incorrect gas/refund logic, and execution-path mistakes in handlers such as CALL and CREATE. The samples cover five opcode semantic families: arithmetic and bitwise operations, memory and storage operations, gas and refund logic, call/create paths, and environment/context-dependent behavior. To avoid retrieval leakage, reference examples used by the retrieval module are isolated from target samples by source-file identity and opcode unit. Thus, the retrieved examples provide semantic anchors for modeling without directly exposing the target mutation. 2) Positive Samples: In addition to negative samples, we use original non-mutated implementation units for internal sanity checking and executability analysis. The main reported effectiveness results focus on the 95 negative samples. C. Baselines We compare VeriSynth with the following baselines. LLM-only. This baseline directly asks the LLM to identify the bug or generate a verification script without semantic decomposition, retrieved examples, opcode-aware prompts, Z3-backed validation, or structured auto-repair. It represents the simplest LLM-based setting. Conversational LLM. This baseline allows the model to revise its output using compiler or solver feedback. However, it does not use retrieved semantic anchors or structured repair actions. This baseline is used to evaluate whether feedback alone is sufficient for robust verification model construction. Handwritten Rust tests. For practical comparison, we use Scroll’s handwritten Rust mutation-test workflow as an engineering baseline. For each sample, the mapped Rust source file is patched, the corresponding cargo test entry is executed, and the original implementation is restored after the test. We count both assertion failures and compilation failures as successful exposures, since both prevent the mutated implementation from passing the test workflow. This baseline is used in RQ5. VeriSynth. The full system includes semantic decomposition, retrieval-guided constraint synthesis, opcode-aware prompting, executable Z3 verification, and auto-repair. D. Evaluation Metrics We use the following metrics to evaluate effectiveness and cost. Detection Rate (DR). DR measures the fraction of negative samples correctly identified as semantically inconsistent: DR =

Ndetected . Nnegative

A bug is considered detected when the synthesized verification model is executable and the SMT solver finds a counterexample (Cu ∧¬Φu satisfiable), indicating a semantic inconsistency between the encoded constraints and the safety obligations.

TABLE III OVERALL BUG DETECTION EFFECTIVENESS ON THE 95- SAMPLE BENCHMARK .

Approach LLM-only Conversational LLM VeriSynth

Detected / Total 44 / 95 58 / 95 87 / 95

DR 46.3% 61.1% 91.6%

Detection rate is reported on negative samples only; systematic false-alarm estimation on positive samples is deferred to future work. Executability Rate (ER). ER measures the fraction of generated verification models that can be successfully compiled and executed: Nexecutable . ER = Ntotal Token Cost. We report the average token usage per sample and estimate the total token consumption for one full benchmark run. This metric reflects the cost of LLM-based synthesis and repair. V. E XPERIMENTAL R ESULTS This section reports the experimental results of VeriSynth. We organize the results according to the five research questions introduced in Section IV. Overall, the results show that VeriSynth substantially outperforms LLM-only baselines in opcode-level bug detection, remains effective across different opcode semantic families, and benefits from each major component in the pipeline. We further analyze the token cost of the framework and compare its practical value with Scroll’s handwritten Rust mutation-test workflow. A. RQ1: Overall Bug Detection Effectiveness RQ1 evaluates whether VeriSynth can effectively detect injected opcode-level semantic bugs. We conduct the experiment on the 95-sample negative benchmark. Each sample contains one localized opcode-related bug, such as an incorrect arithmetic rule, missing state update, wrong boundary condition, incorrect gas/refund logic, or execution-path error in handlers such as CALL and CREATE. We compare VeriSynth with the baselines described in Section 4.3: LLM-only, Conversational LLM, and Handwritten Rust tests (for RQ5). The conversational baseline is inspired by feedback-driven LLM repair settings [23]. As shown in Table III, VeriSynth detects 87 out of 95 injected bugs, achieving a detection rate of 91.6% (DR defined in Section 4.4). In contrast, the LLM-only baseline detects only 44 bugs, corresponding to a detection rate of 46.3%. Although the conversational baseline improves over LLM-only generation by using feedback, it still detects only 58 bugs. These results indicate that feedback alone is insufficient for reliable verification model construction. The improvement of VeriSynth comes from the combination of semantic decomposition, retrieval-grounded modeling, opcode-aware prompts, and solver-guided repair.

TABLE IV B UG DETECTION RESULTS ACROSS OPCODE SEMANTIC FAMILIES .

Opcode Family Arithmetic and Bitwise Memory and Storage Gas and Refund Call/Create Paths Environment and Context Overall

Detected / Total 21 / 22 24 / 26 14 / 15 18 / 21 10 / 11 87 / 95

DR 95.5% 92.3% 93.3% 85.7% 90.9% 91.6%

The result also supports our central design choice: LLMs should not be used as final bug judges. Instead, they are more effective when used as semantic model constructors, while the final validation is performed by an SMT solver. This distinction explains why VeriSynth outperforms direct LLMbased detection. RQ1: VeriSynth detects 87 out of 95 injected opcode-level bugs, achieving a detection rate of 91.6%. This substantially outperforms LLM-only detection and conversational LLM repair, showing the effectiveness of solver-backed verification model synthesis. B. RQ2: Effectiveness Across Opcode Semantic Families RQ2 investigates whether VeriSynth remains effective across different opcode semantic families. This question is important because zkEVM implementation bugs are not limited to simple arithmetic operations. Many difficult cases involve storage updates, memory behavior, call/create execution paths, gas accounting, and environment-dependent logic. Therefore, we divide the 95 negative samples into five semantic families and report the detection results for each family. Table IV shows that VeriSynth performs well across all semantic families. The highest detection rate is achieved on arithmetic and bitwise operations, where the state transition is relatively local and can be naturally encoded using bitvector constraints. The framework also performs strongly on memory/storage and gas/refund cases, demonstrating that it can model nontrivial state changes beyond simple numerical operations. The most challenging category is call/create paths, where VeriSynth detects 18 out of 21 bugs. This lower detection rate is expected because call/create semantics involve multiple interacting components, including execution context, return values, address creation, memory effects, and failure propagation. Even in this category, VeriSynth still achieves an 85.7% detection rate, suggesting that the proposed semantic decomposition and retrieval grounding are useful for complex opcode-level behaviors. RQ2: VeriSynth remains effective across different opcode semantic families. While call/create paths are more challenging than arithmetic operations, the framework still detects most injected bugs in complex state-transition scenarios.

TABLE V A BLATION STUDY OF V ERI S YNTH COMPONENTS ON THE 95- SAMPLE BENCHMARK .

Variant w/o Decomposition w/o Retrieval w/o Opcode-aware Prompt w/o Auto-Repair w/o Z3 Validation Full VeriSynth

Detected / Total 72 / 95 68 / 95 74 / 95 63 / 95 45 / 95 87 / 95

DR 75.8% 71.6% 77.9% 66.3% 47.4% 91.6%

ER 81.1% 78.9% 84.2% 66.3% – 93.7%

C. RQ3: Ablation Study RQ3 evaluates the contribution of each major component in VeriSynth. We consider five ablated variants. The first removes semantic decomposition and directly feeds larger code fragments to the LLM. The second removes retrieval grounding and generates verification models without semantically similar reference examples. The third removes opcodeaware prompting and uses a generic prompt for all opcode families. The fourth removes auto-repair and accepts only the initially generated verification model. The fifth removes Z3 validation, reducing the system to an LLM-only judgment setting. Table V shows that removing any major component reduces the final performance. The largest drop occurs when autorepair is removed. Without auto-repair, the detection rate decreases from 91.6% to 66.3%, and the executability rate also drops to 66.3%. This indicates that many initially generated Python/Z3 scripts are semantically close to the desired model but fail due to local syntax errors, missing declarations, invalid solver API usage, or bit-vector sort mismatches. The repair loop is therefore essential for turning near-valid candidate models into executable verification artifacts. Qualitatively, most repair actions addressed parse and sort errors (missing declarations, bit-vector width mismatches), while fewer involved semantic counterexample-guided refinement. Removing retrieval grounding also causes a clear performance drop, reducing the detection rate to 71.6%. Without retrieved examples, the LLM is more likely to produce inconsistent symbolic variables, incomplete transition relations, or missing resource constraints. This confirms that retrieval acts as a modeling prior rather than ordinary context augmentation. Removing semantic decomposition reduces the detection rate to 75.8%. This variant particularly struggles with complex opcode handlers, where relevant state effects are scattered across helper routines, state objects, and conditional branches. By contrast, semantic decomposition isolates verificationrelevant units and makes the model synthesis task more tractable. Removing opcode-aware prompting reduces the detection rate to 77.9%. This result suggests that generic prompts are insufficient for diverse opcode families. Arithmetic operations, storage updates, gas accounting, and call/create paths require different symbolic state schemas and modeling obligations.

TABLE VI T OKEN COST OF V ERI S YNTH ON THE 95- SAMPLE BENCHMARK .

Metric Benchmark size Backend model Average tokens per sample Estimated total tokens Average repair rounds Maximum repair budget

Value 95 samples GPT-4o ∼100K ∼9.5M 1.8 3

Finally, the variant without Z3 validation detects only 45 out of 95 bugs. This result is close to the LLM-only baseline and confirms that the final judgment must remain solver-backed. The LLM can propose candidate models, but Z3 is necessary for reliable verification. RQ3: All major components contribute to the effectiveness of VeriSynth. Auto-repair has the largest impact on executability, while retrieval and decomposition improve semantic consistency and robustness on complex opcode handlers.

D. RQ4: Token Cost Analysis RQ4 analyzes the token cost of VeriSynth. Since the current prototype relies on LLM calls for constraint synthesis and repair, token usage is an important practical factor. We therefore measure the average token consumption per sample and estimate the total cost for one full run over the 95-sample benchmark. As shown in Table VI, each sample consumes approximately 100K tokens on average. This includes the target semantic unit, retrieved anchors, opcode-aware modeling instructions, generated Python/Z3 scripts, compiler diagnostics, solver feedback, and repair prompts. For the 95-sample benchmark, the estimated total token usage is approximately 9.5M tokens. The token cost is nontrivial. However, it is bounded by the repair budget and predictable in practice. In our current setting, the maximum number of repair iterations is limited to 3, and the average number of repair rounds is 1.8. This suggests that most failed generations can be repaired within a small number of iterations. It is also important to note that VeriSynth is designed for offline verification of security-critical implementation logic rather than online per-transaction execution. Therefore, the token overhead is acceptable for scenarios such as opcode implementation review, regression checking after code changes, and validation of high-risk state-transition logic. Compared with the manual effort required to construct Python/Z3 verification models, the LLM cost provides a practical tradeoff between automation and verification rigor.

TABLE VII P RACTICAL COMPARISON WITH S CROLL’ S HANDWRITTEN RUST TESTS .

Bug Group Opcode semantic errors Opcode execution-path errors Overall

Total 75 20

Handwritten 44 11

VeriSynth 69 18

95

55

87

Fig. 3. Practical comparison between handwritten Rust tests and VeriSynth by bug category on the test_neg benchmark.

RQ4: Each sample consumes approximately 100K tokens on average, resulting in about 9.5M tokens for the 95sample benchmark. Although the cost is nontrivial, it remains bounded by the repair budget and is suitable for offline verification of security-critical zkEVM implementation logic. E. RQ5: Practical Value Compared with Handwritten Rust Tests RQ5 evaluates whether VeriSynth provides practical value beyond a handwritten Rust mutation-test workflow. For this comparison, we report results grouped into two high-level categories that complement the per-family breakdown in RQ2: opcode semantic errors (spanning arithmetic, memory/storage, gas/refund, and environment families) and opcode executionpath errors (spanning call/create path and branch logic). For each negative sample, the handwritten baseline temporarily patches the mapped Scroll source file, runs the corresponding cargo test entry in the original crate environment, and then restores the original implementation. This baseline reflects a realistic engineering workflow: it uses tests that are already maintained with the project, but its effectiveness is bounded by the assertions and execution cases that developers have manually written. Table VII and Fig. 3 report the comparison on our 95-sample negative benchmark, denoted as test_neg. The handwritten Rust workflow exposes 55 injected bugs, while VeriSynth detects 87. The gap is consistent across both groups: for opcode semantic errors, handwritten tests expose 44 out of 75 cases, whereas VeriSynth detects 69; for opcode executionpath errors, handwritten tests expose 11 out of 20 cases, whereas VeriSynth detects 18. Overall, this corresponds to a

detection rate of 57.9% for handwritten tests and 91.6% for VeriSynth. Even under this counting (see Section 4.3), handwritten tests leave a substantial fraction of negative samples unexposed. VeriSynth improves coverage by synthesizing explicit semantic constraints and checking them with Z3, which makes it less dependent on whether a particular behavior has already been encoded as a manual unit-test assertion. RQ5: Compared with Scroll’s handwritten Rust mutationtest workflow, VeriSynth detects 87 bugs on test_neg, while handwritten tests expose 55. The improvement across both semantic and execution-path bug groups indicates that VeriSynth is a practical complement to manually maintained Rust tests. VI. R ELATED W ORK A. Formal Semantics and Verification of EVMs A substantial body of work has studied the formal semantics and verification of Ethereum programs. KEVM provides an executable formal semantics of the EVM in the K framework and enables reasoning about bytecode-level execution [6]. Tools such as ZEUS and Securify analyze smart contracts against predefined safety properties using abstract interpretation, symbolic reasoning, or compliance and violation patterns [4], [5]. These approaches primarily target smart contracts or EVM bytecode and generally assume that the underlying virtualmachine implementation correctly realizes the intended semantics. Recent work has also examined the soundness and completeness of zkEVM constraint systems. For example, automated vetting techniques detect under-constrained or overconstrained behaviors in zkEVM circuits and witness generation [20]. Such work is complementary to VeriSynth: circuit-level verification checks whether a proving system correctly constrains its witnesses, whereas VeriSynth focuses on whether source-level Rust opcode handlers correctly implement the intended state transitions. In addition, existing formal-verification approaches usually require manually written semantics or properties. VeriSynth instead synthesizes executable Python/Z3 models directly from source-level implementations. B. Testing and Validation of EVM Implementations Production EVM and zkEVM projects rely extensively on unit tests, integration tests, official Ethereum execution vectors, and regression testing. These techniques are effective for checking known corner cases and preventing previously discovered defects from reappearing. Mutation testing can further evaluate whether a test suite exposes deliberately injected implementation faults. Differential testing provides another practical validation strategy. EVMFuzz, for example, generates and mutates contract inputs and compares the resulting executions across different EVM implementations [25]. Disagreements in return values, traces, or gas consumption can reveal implementation defects. However, testing and fuzzing reason about a finite set

of concrete executions, and their effectiveness depends on the selected inputs, assertions, and comparison oracles. Bugs involving uncommon storage states, gas boundaries, exceptional branches, or interactions between execution components may therefore remain unexposed. VeriSynth complements these techniques by constructing symbolic transition models and using SMT-generated counterexamples to reason about classes of executions rather than individual test inputs. C. Large Language Models for Software Engineering Large language models (LLMs) have been increasingly applied to software engineering tasks, including code understanding, code generation, test generation, program repair, and code summarization [18], [21], [22], [24]. Their in-context learning ability allows developers to provide task descriptions, demonstrations, and feedback through prompts [18], [19]. Instruction tuning and reasoning-oriented prompting can further improve the controllability and consistency of generated artifacts [26]–[28]. Recent studies have extended these capabilities to formal specification generation. SpecGen generates program specifications from source code, while PropertyGPT combines retrieval with LLM generation to infer properties for smart contracts [16], [17]. These approaches mainly produce declarative properties or annotations, whereas zkEVM verification requires executable models that encode complete state transitions across multiple execution-state components. LLMs have also been used to improve software artifacts through execution feedback. Conversational automated program repair, for example, iteratively revises candidate patches using compiler errors, test failures, and runtime diagnostics [23]. However, LLM-generated verification models may contain hallucinated semantics, omitted path conditions, inconsistent symbolic types, or invalid solver operations. Consequently, our goal is not to use an LLM as a direct bug detector or correctness oracle. Instead, VeriSynth uses the LLM as a formalization frontend that translates implementation-level opcode semantics into executable SMT-based verification models. Semantic decomposition and retrieval-grounded prompting guide model generation, while compiler diagnostics and solver feedback support bounded auto-repair. The final correctness decision is always made by the SMT solver. VII. C ONCLUSION We introduced VeriSynth, an LLM-guided framework that synthesizes executable Python/Z3 verification models from zkEVM Rust source code by combining semantic decomposition, retrieval-grounded prompting, and verification-guided auto-repair. On our self-constructed benchmark of 95 injected opcode-level bugs, VeriSynth detects 91.6%, outperforming direct LLM baselines (46.3–61.1%) and Scroll’s handwritten mutation-test suite (57.9%). Our framework remains effective across all five opcode semantic families, including complex call/create paths (85.7%). Ablation confirms that auto-repair contributes the largest gain in executability, followed by retrieval grounding. Compared with Scroll’s handwritten tests, VeriSynth detects 32 additional

bugs, indicating that automated constraint synthesis complements manual testing. Future work includes systematic false-alarm estimation on positive samples, cross-project validation on additional zkEVM implementations, and cost reduction through smaller model distillation. R EFERENCES [1] Ethereum Foundation, “Zero-knowledge rollups,” https://ethereum.org/en/developers/docs/scaling/zk-rollups/, accessed: 2026-06-27. [2] G. Wood, “Ethereum: A secure decentralised generalised transaction ledger,” Ethereum Yellow Paper, 2014. [Online]. Available: https://ethereum.github.io/yellowpaper/paper.pdf [3] L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making smart contracts smarter,” in Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016, pp. 254–269. [4] P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. Buenzli, and M. Vechev, “Securify: Practical security analysis of smart contracts,” in Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018, pp. 67–82. [5] S. Kalra, S. Goel, M. Dhawan, and S. Sharma, “Zeus: Analyzing safety of smart contracts,” in Proceedings of the Network and Distributed System Security Symposium, 2018. [6] E. Hildenbrandt, M. Saxena, N. Rodrigues, X. Zhu, P. Daian, D. Guth, B. M. Moore, D. Park, Y. Zhang, A. Stefanescu, and G. Rosu, “Kevm: A complete formal semantics of the ethereum virtual machine,” in Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018, pp. 204–217. [7] L. de Moura and N. Bjørner, “Z3: An efficient smt solver,” in Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008, pp. 337–340. [8] C. Barrett, A. Stump, and C. Tinelli, “The smt-lib standard: Version 2.0,” Department of Computer Science, The University of Iowa, Tech. Rep., 2010. [Online]. Available: http://smtlib.cs.uiowa.edu/ [9] C. Cadar, D. Dunbar, and D. Engler, “Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs,” in Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation, 2008, pp. 209–224. [10] D. Kroening, E. Clarke, and F. Lerda, “A tool for checking ansi-c programs,” in Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2004, pp. 168–176. [11] J. C. King, “Symbolic execution and program testing,” in Communications of the ACM, vol. 19, no. 7, 1976, pp. 385–394. [12] M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin, “Dynamically discovering likely program invariants to support program evolution,” IEEE Transactions on Software Engineering, vol. 27, no. 2, pp. 99–123, 2001. [13] C. Flanagan and K. R. M. Leino, “Houdini, an annotation assistant for esc/java,” in Proceedings of the International Symposium of Formal Methods Europe, 2001, pp. 500–517. [14] P. Tolmach, Y. Li, S.-W. Lin, Y. Liu, and Z. Li, “A survey of smart contract formal specification and verification,” arXiv preprint arXiv:2008.02712, 2020. [Online]. Available: https://arxiv.org/abs/2008.02712

[15] F. Salzano, C. K. Antenucci, S. Scalabrino, G. Rosa, R. Oliveto, and R. Pareschi, “An empirical analysis of vulnerability detection tools for solidity smart contracts using line level manually annotated vulnerabilities,” Empirical Software Engineering, vol. 31, no. 5, p. 143, 2026. [16] L. Ma, S. Liu, Y. Li, X. Xie, and L. Bu, “Specgen: Automated generation of formal program specifications via large language models,” in Proceedings of the 47th IEEE/ACM International Conference on Software Engineering, 2025. [17] Y. Liu, Y. Li, L. Ma, and Y. Liu, “Propertygpt: Llm-driven formal verification of smart contracts through retrieval-augmented property generation,” arXiv preprint arXiv:2405.02580, 2024. [Online]. Available: https://arxiv.org/abs/2405.02580 [18] T. B. Brown, B. Mann, N. Ryder, M. Subbiah, J. Kaplan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askell et al., “Language models are few-shot learners,” Advances in Neural Information Processing Systems, vol. 33, pp. 1877–1901, 2020. [19] J. White, Q. Fu, S. Hays, M. Sandborn, C. Olea, H. Gilbert, A. Elnashar, J. Spencer-Smith, and D. C. Schmidt, “A prompt pattern catalog to enhance prompt engineering with chatgpt,” in Proceedings of the 30th Conference on Pattern Languages of Programs, 2023. [20] X. Peng, Z. Sun, K. Zhao, Z. Ma, Z. Li, J. Jiang, X. Luo, and Y. Zhang, “Automated soundness and completeness vetting of polygon {zkEVM},” in 34th USENIX Security Symposium (USENIX Security 25), 2025, pp. 4093–4108. [21] M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. de Oliveira Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman et al., “Evaluating large language models trained on code,” arXiv preprint arXiv:2107.03374, 2021. [Online]. Available: https://arxiv.org/abs/2107.03374 [22] X. Hou, Y. Zhao, Y. Liu, Z. Yang, K. Wang, L. Li, X. Luo, D. Lo, J. Grundy, and H. Wang, “Large language models for software engineering: A systematic literature review,” arXiv preprint arXiv:2308.10620, 2023. [Online]. Available: https://arxiv.org/abs/2308.10620 [23] C. S. Xia and L. Zhang, “Conversational automated program repair,” arXiv preprint arXiv:2301.13246, 2023. [Online]. Available: https://arxiv.org/abs/2301.13246 [24] OpenAI, “Gpt-4 technical report,” arXiv preprint arXiv:2303.08774, 2023. [Online]. Available: https://arxiv.org/abs/2303.08774 [25] Y. Fu, M. Ren, F. Ma, X. Yang, H. Shi, S. Li, and X. Liao, “Evmfuzz: Differential fuzz testing of ethereum virtual machine,” Journal of Software: Evolution and Process, vol. 36, no. 4, p. e2556, 2024. [26] L. Ouyang, J. Wu, X. Jiang, D. Almeida, C. Wainwright, P. Mishkin, C. Zhang, S. Agarwal, K. Slama, A. Ray et al., “Training language models to follow instructions with human feedback,” in Advances in Neural Information Processing Systems, 2022, pp. 27 730–27 744. [27] J. Wei, X. Wang, D. Schuurmans, M. Bosma, F. Xia, E. Chi, Q. V. Le, and D. Zhou, “Chain-of-thought prompting elicits reasoning in large language models,” in Advances in Neural Information Processing Systems, 2022, pp. 24 824–24 837. [28] X. Wang, J. Wei, D. Schuurmans, Q. V. Le, E. H. Chi, S. Narang, A. Chowdhery, and D. Zhou, “Self-consistency improves chain of thought reasoning in language models,” in Proceedings of the International Conference on Learning Representations, 2023.