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

• URL: http://arxiv.org/abs/2607.19795v1
• Date: Wed, 22 Jul 2026 06:20:36 GMT
• Title: Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis
• Abstract summary: ZkEVMs generate zero-knowledge that guarantee off-chain execution correctness.<n> subtle implementation bugs can lead to valid proofs certifying semantically faulty states.<n>Formal verification via SMT solvers can prevent this, but is bottlenecked by specification.<n>We propose Veri Synth, a framework that synthesizes executable Python/Z3 verification models from Rust.
• Score: 14.825615940318038
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Zero-Knowledge Ethereum Virtual Machines (zkEVMs) secure Ethereum rollups by generating zero-knowledge 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 auto-repair 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.

Related papers

• Weave of Formal Thought [51.56484100374058]
  We introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations.<n>We present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation.<n>For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline.
  arXiv  Detail & Related papers  (2026-06-24T15:58:11Z)
• Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering [40.048798975817924]
  Vibe coding is fast and may be adequate for low-criticality consumer software.<n>For safety-critical systems governed by DO-178C, IEC 61508, or ISO 26262, it offers no path to certification.<n>We present Forge, a closed-loop pipeline that guides vibe coding through formal verification.
  arXiv  Detail & Related papers  (2026-06-21T10:01:45Z)
• SimSD: Simple Speculative Decoding in Diffusion Language Models [61.33773959352141]
  Diffusion large language models (dLLMs) offer faster inference through parallel or blockwise decoding.<n>Their masked language modeling formulation remains incompatible with standard token-level speculative decoding.<n>We propose a speculative decoding algorithm for dLLMs, named SimSD, that equips dLLMs with temporally valid token-level contexts.<n>Our method achieves up to 7.46x higher decoding throughput while maintaining and even improving average generation quality.
  arXiv  Detail & Related papers  (2026-06-01T17:46:46Z)
• Towards Human-Like Interactive Speech Recognition With Agentic Correction and Semantic Evaluation [53.844308305341166]
  We propose textbfAgentic ASR, a closed-loop framework that combines a single-pass ASR front-end with semantic correction, intent routing, and reasoning-based editing.<n> Experiments on multilingual, named-entity-intensive, and code-switching benchmarks show that iterative interaction consistently reduces semantic errors.
  arXiv  Detail & Related papers  (2026-05-28T06:23:31Z)
• Agentic Model Checking [12.832868209928039]
  We propose a paradigm that couples LLM agents with a bounded model checking backend.<n>We instantiate the approach in BMC-Agent and evaluate it on LLM-generated kernel and compiler code in C and Rust.
  arXiv  Detail & Related papers  (2026-05-20T17:25:52Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Certified Program Synthesis with a Multi-Modal Verifier [5.998029529040967]
  LeetProof is an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean.<n>It combines dynamic validation, automated proofs, and interactive proof scripting in one foundational framework.<n>We evaluate LeetProof on benchmarks derived from prior work on certified synthesis.
  arXiv  Detail & Related papers  (2026-04-17T14:56:45Z)
• SEVerA: Verified Synthesis of Self-Evolving Agents [12.9624447364193]
  Self-evolving agent frameworks provide no formal guarantees of safety or correctness.<n>We formulate agentic code generation as a constrained learning problem, combining hard formal specifications with soft objectives capturing task utility.<n>We present SEVerA, a three-stage framework: Search synthesizes candidate parametric programs containing FGGM calls; Verification proves correctness with respect to hard constraints for all parameter values, reducing the problem to unconstrained learning.
  arXiv  Detail & Related papers  (2026-03-26T07:32:20Z)
• zkCraft: Prompt-Guided LLM as a Zero-Shot Mutation Pattern Oracle for TCCT-Powered ZK Fuzzing [7.274627641804014]
  zkCraft is a framework that combines deterministic, R1CS-aware localization with proof-bearing search to detect semantic inconsistencies.<n>We show that proof-bearing localization detects diverse under- and over-constrained faults with low false positives and reduces costly solver interaction.
  arXiv  Detail & Related papers  (2026-01-31T11:31:00Z)
• From Completion to Editing: Unlocking Context-Aware Code Infilling via Search-and-Replace Instruction Tuning [81.97788535387286]
  We propose a framework that internalizes the agentic verification-and-editing mechanism into a unified, single-pass inference process.<n>With minimal data, SRI-Coder enables Chat models to surpass the completion performance of their Base counterparts.<n>Unlike FIM-style tuning, SRI preserves general coding competencies and maintains inference latency comparable to standard FIM.
  arXiv  Detail & Related papers  (2026-01-19T20:33:53Z)
• $\ exttt{SEM-CTRL}$: Semantically Controlled Decoding [53.86639808659575]
  $texttSEM-CTRL$ is a unified approach that enforces rich context-sensitive constraints and task- and instance-specific semantics directly on an LLM decoder.<n>texttSEM-CTRL$ allows small pre-trained LLMs to efficiently outperform larger variants and state-of-the-art reasoning models.
  arXiv  Detail & Related papers  (2025-03-03T18:33:46Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.