Pith. sign in

REVIEW 4 major objections 5 minor 28 references

By keeping the LLM as a formalization frontend and making Z3 the judge, VeriSynth detects 87 of 95 injected zkEVM opcode bugs, beating both LLM-only detection and a handwritten mutation-test suite.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 11:42 UTC pith:WEFAEV4O

load-bearing objection Useful, well-ablated framework for LLM-guided model synthesis, but the headline detection rate is unvalidated because the obligations lack an external semantic anchor. the 4 major comments →

arxiv 2607.19795 v1 pith:WEFAEV4O submitted 2026-07-22 cs.SE

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

Shichen Huang , Zhenghe Jiang , Yi Jiang , Ling-I Wu , Jingyang Li , Guoqiang Li This is my paper
classification cs.SE
keywords formal verificationLLM-guided synthesisconstraint synthesisSMT solverzkEVMRust opcodespecification bottleneckmutant detection
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

VeriSynth turns Rust implementations of zkEVM opcode handlers into executable symbolic models so that an SMT solver, not a human, can check them for semantic bugs. The paper's core claim is that the specification bottleneck blocking zkEVM formal verification can be automated by a strict division of labor: the LLM only translates code into candidate constraints, and Z3 renders the final verdict. On a new benchmark of 95 mutated opcode handlers spanning five semantic families, the framework detects 87 bugs (91.6%), far above direct LLM judgment (46.3%) and a conversational baseline (61.1%), and it also beats a production handwritten mutation-test suite, which caught 55. The authors conclude that solver-backed verification of zkEVM source is practical and that the pipeline generalizes across opcode families, with call/create paths being the hardest (85.7%). The significance is that subtle gas and state-update defects in rollup infrastructure can be caught by searching over entire classes of executions rather than by test cases developers happen to anticipate.

Core claim

VeriSynth synthesizes executable Python/Z3 verification models directly from zkEVM Rust opcode handlers, avoiding hand-written specifications. The paper's central claim is that a strict 'LLM proposes, solver decides' division — the LLM writes candidate constraints over stack, memory, storage, gas, refund, and context; Z3 checks them against independent safety obligations — makes automated formal verification practical. The check is satisfiability of C_u ∧ ¬Φ_u; a counterexample is a detected bug, unsatisfiability is a certificate within the abstraction. On 95 injected opcode mutants, VeriSynth detects 87 (91.6%), versus 44 (46.3%) for LLM-only and 58 (61.1%) for a conversational baseline, an

What carries the argument

The central mechanism is the verification model M_u = ⟨V_u, C_u, Φ_u⟩ plus the satisfiability query C_u ∧ ¬Φ_u. V_u declares symbolic variables for the zkEVM state; C_u encodes the implementation as guarded constraints with explicit frame conditions; Φ_u is the safety obligation, intended to be independent of both the target code and the LLM's beliefs. A solver counterexample is a detected bug and drives repair; unsatisfiability is a correctness certificate within the abstraction. Three components make this tractable: semantic decomposition groups each state transition into one coherent unit; retrieval-grounded prompting anchors variables and solver APIs to previously verified models; and ve

Load-bearing premise

The entire method assumes the safety obligations Φ_u encode the intended opcode semantics correctly, independent of the implementation and of the LLM; nothing outside the authors' judgment is given as the authority for what 'correct' means, so a shared misunderstanding would sail through the solver.

What would settle it

Run VeriSynth on the same 95 mutants while independently computing, for each mutant, whether execution diverges from a trusted reference EVM on a broad set of symbolic states; if the solver's satisfiable/unsatisfiable verdicts do not track that divergence — or if the 8 missed mutants and the 87 flagged ones are largely inconsistent with the reference — the claimed arbitration of correctness does not hold.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

If this is right

  • If correct, zkEVM verification no longer needs hand-written formal specs: opcode handlers can be checked automatically during development, catching gas, storage, and control-flow bugs before they enter proof circuits.
  • LLM-based bug detection should not be used as a judge: the gap between 46.3% (LLM-only) and 91.6% (VeriSynth) shows the solver, not the model, is what makes findings trustworthy, reshaping tool design for LLM verification.
  • The framework complements existing test suites: it detected 32 bugs that Scroll's handwritten mutation tests missed on the same benchmark, so it is a viable addition to regression and review pipelines.
  • The approach is not limited to simple arithmetic: it retains 85.7% to 95.5% detection across all five semantic families, including the complex call/create paths.
  • The bounded cost — about 100K tokens and 1.8 repair rounds per opcode — makes offline use feasible, and the paper's own future-work directions point toward distillation reducing it further.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The paper claims Φ is built from 'validated opcode semantics' but never specifies the validator or anchors it to an independent, externally reviewed semantics; if the authors' and the LLM's shared beliefs about EVM gas or refund rules are wrong, the solver certifies internal consistency rather than real correctness.
  • A direct test of the claim would be to run the same 95 mutants through a differential oracle against an independent EVM executor and measure how well the solver's satisfiable/unsatisfiable verdicts track true semantic divergence; the agreement rate would separate genuine arbitration from agreement with the authors' expectations.
  • The 'LLM proposes, solver decides' scheme is a general recipe: any low-level system whose verification bottleneck is model synthesis — other VM implementations, hardware models, protocol state machines — could reuse the same decomposition and repair loop, provided its safety obligations can be stated independently.
  • Because the benchmark is self-constructed and no false-alarm rate is reported on unmutated code, the practical safety of running VeriSynth in CI without human triage is unmeasured; computing the positive-sample false-positive rate is the natural next experimental step.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. VeriSynth is an LLM-guided framework that synthesizes executable Python/Z3 verification models from zkEVM Rust opcode handlers. The pipeline decomposes a handler into semantic units, retrieves similar verified models from a reference database, prompts an LLM to emit candidate SMT constraints, and then uses Z3 to check the query C_u ∧ ¬Φ_u. The paper reports that this approach detects 87/95 injected semantic bugs (91.6%), outperforming direct LLM baselines (46.3%) and conversational LLM repair (61.1%), and also outperforming Scroll's handwritten Rust mutation tests (55/95). Ablations show that auto-repair, retrieval grounding, semantic decomposition, opcode-aware prompting, and Z3 validation each contribute to the reported results. The authors explicitly defer systematic false-alarm estimation on positive samples to future work.

Significance. If the central claim is validated, the paper makes a useful contribution: it proposes a practical division of labor between an LLM formalization frontend and an SMT decision backend, introduces a source-level zkEVM verification benchmark, and reports systematic ablations that give engineering insight into what makes LLM-driven verification-model synthesis work. The paper also includes a concrete comparison with an industrial handwritten-test workflow. However, the headline 'bug detection rate' is only as strong as the semantic obligations encoded in Φ_u, and the paper currently lacks the independent semantic oracle and the positive-sample false-alarm control needed to establish that the reported 91.6% reflects genuine detection of EVM-semantics violations rather than consistency between two LLM-influenced artifacts.

major comments (4)
  1. [§III-A, Eq. (2)] The verification query C_u ∧ ¬Φ_u is sound only if Φ_u correctly encodes intended EVM semantics independently of the target code and of the LLM's own beliefs. The paper says Φ_u is 'constructed from validated opcode semantics and family-specific consistency rules,' but 'validated' is never defined: no external formal semantics (e.g., KEVM or the Yellow Paper) is used as an oracle, and the reference database D in §III-B is populated by models that pass obligations that are themselves LLM-generated and self-validated. Z3 therefore checks internal consistency between two LLM-influenced artifacts, not correctness against an independent semantic standard. This is the load-bearing gap for the paper's central claim.
  2. [§IV-D, note under Table III] Systematic false-alarm estimation on non-mutated (positive) units is explicitly deferred to future work. Without this control, the 87/95 figure cannot be interpreted as a bug-detection rate: a satisfiable query can arise from an over-strong Φ_u or an unfaithful C_u, and an unsatisfiable query can mask a bug when the same semantic misconception enters both sides. The paper should report false positives on the original, non-mutated handlers and, ideally, use an independently anchored Φ_u (e.g., derived from KEVM or a hand-written formal semantics) to break the circularity.
  3. [§III-B] The retrieval database D is self-validated: a reference model is added only after passing syntax checking, sort checking, solver execution, and 'the associated semantic obligations,' but those obligations are generated by the same LLM-influenced pipeline. If any misconception is encoded in the database, retrieval will propagate it to future units, potentially creating false positives and false negatives. The paper should specify how the semantic obligations used to validate D are themselves validated, or use an independent source of semantic truth (e.g., an existing formal EVM semantics) for at least a held-out subset.
  4. [§IV-B] The benchmark construction is underspecified. The paper states that 95 negative samples were created by injecting one bug per target unit across five opcode semantic families, but does not describe how mutations were generated, whether they were human-validated against the intended EVM semantics, how representative they are of real zkEVM bugs, or whether any are detectable from syntax/sorts alone. Without this detail, the external validity of the 91.6% detection rate and the comparison against handwritten tests is difficult to assess.
minor comments (5)
  1. [§IV-A] The paper refers to 'Section 4.3' and 'Section 4.4' in the results section; the cross-references should use the Roman-numeral section style (e.g., §IV-C, §IV-D) for consistency.
  2. [Table VI] The token cost of ~100K tokens per sample is nontrivial. Please specify what is included in the count (prompt, generated model, repair feedback) and whether the reported figure includes the retrieval context or only the synthesis/repair calls.
  3. [§V-E, Fig. 3] Figure 3 is referenced but the text does not explain what the figure shows beyond the table; please add a descriptive caption and refer to it explicitly in the text.
  4. [§IV-B] The dataset name 'test_neg' appears in §V-E but is not defined when the dataset is introduced. Please define it and any companion 'test_pos' set at first use.
  5. [References] The paper compares against 'Scroll's handwritten Rust mutation-test workflow' but the cited reference [14] is a survey on smart contract verification, not a source for Scroll's tests. Please cite the actual repository or documentation for the handwritten mutation tests.

Circularity Check

2 steps flagged

The 91.6% "bug detection rate" is operationally a self-consistency rate between two LLM-generated artifacts: Φ_u and the retrieval anchors are validated inside the same loop, and positive-sample false alarms are deferred.

specific steps
  1. self definitional [Section III-A (Eq. 2), Section III-C, Section IV-D (Table III)]
    "Φ_u is constructed from validated opcode semantics and family-specific consistency rules rather than from the target code alone. ... 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. ... A bug is considered detected when the synthesized verification model is executable and the SMT solver finds a counterexample (C_u ∧ ¬Φ_u satisfiable)."

    DR is defined solely as satisfiability of C_u ∧ ¬Φ_u. Both C_u and Φ_u are synthesized by the same LLM in the same prompt: the LLM encodes source behavior and also the safety assertions/obligations, and the only stated validation of Φ_u is that it comes from "validated opcode semantics" whose validation is the self-checked pipeline. No external formal semantics (KEVM, Yellow Paper) anchors Φ_u. Hence a satisfiable query can be produced by an over-strong Φ_u or an unfaithful C_u, and an unsatisfiable query can hide a bug when the same LLM misconception is encoded on both sides. The reported 91.6% therefore measures self-consistency between two LLM-generated artifacts, not conformance to intended EVM semantics; "bug detected" is defined as this internal inconsistency by construction.

  2. other [Section III-B (reference database D)]
    "the retrieved examples serve as semantic anchors for executable model construction. ... 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."

    The reference database D is the grounding that makes Φ_u "validated": retrieval provides semantic anchors for synthesis. But the acceptance criterion for each D entry is that it passes "the associated semantic obligations" — the same LLM-generated, solver-checked consistency obligations that D is supposed to validate. This is bootstrap validation, not an independent oracle. Anchors therefore carry the same unanchored semantics into every new unit, and the loop never consults an external definition of intended EVM behavior, leaving the central detection claim circular.

full rationale

The paper's ablations and baseline comparisons are internally coherent: removing components degrades the metric, and the comparison with Scroll's handwritten tests is an external engineering baseline. However, all of these comparisons use the same self-consistency detection rate as the target metric. A bug is defined as detected iff C_u ∧ ¬Φ_u is satisfiable (Section IV-D), and the only stated construction of Φ_u is from "validated opcode semantics" whose validation reduces to passing LLM-generated semantic obligations in the same pipeline (Section III-B). No KEVM/Yellow-Paper oracle is used to check Φ_u; the paper itself concedes in Section III-D that "an unsatisfiable query establishes correctness only within the modeled state and assumptions." The missing positive-sample false-alarm study, flagged in the Table III note ("systematic false-alarm estimation on positive samples is deferred to future work") and in Section IV-D, is the control that would disambiguate real bug detection from over-strong obligations; deferring it leaves the 91.6% figure unanchored. This is not a self-citation problem: the paper does not rely on the authors' prior theorems. The circularity is in the validation loop: the LLM proposes both sides of Eq. (2), and the solver checks their mutual consistency, which is then labeled bug detection. Score 6 reflects partial but central circularity of the headline metric, not a fully forced derivation.

Axiom & Free-Parameter Ledger

4 free parameters · 6 axioms · 0 invented entities

VeriSynth's central claim rests on obligations Φ_u being correct expressions of intended EVM semantics validated inside the same LLM-influenced loop with no external formal semantics (III-A); on the symbolic abstraction of Eq. 4 being faithful; on the 95 mutations being genuine bugs with correct labels; on GPT-4o not benefiting from pretraining exposure to the underlying public zkEVM code; and on Z3 soundness. The free parameters are pipeline hyperparameters (α, k, T_max=3, timeouts) — hand-chosen, not fitted to the benchmark, which counts in the paper's favor. No new physical entities are posited; 'semantic unit' and 'reference database' are engineering abstractions, so invented_entities is empty.

free parameters (4)
  • α (similarity blend weight, Eq. 3)
    Hand-chosen weight blending embedding cosine similarity and family match in SIM(u,d); value not reported. Affects which anchors are retrieved and hence the generated models.
  • k (retrieval count)
    Top-k anchors per unit (III-B); value not reported. Affects grounding strength and token cost.
  • T_max (repair budget) = 3
    Maximum repair iterations, stated in IV-A; average repair rounds 1.8 (Table VI) is a measurement, not a fitted parameter.
  • Solver timeout / bounds
    A bounded timeout per query is mentioned in III-D but no value is given; affects whether semantic counterexamples are found within budget.
axioms (6)
  • domain assumption Φ_u correctly encodes intended EVM opcode semantics ('validated opcode semantics and family-specific consistency rules')
    Section III-A, Eq. 2: the obligations are asserted to be validated, but no external formal semantics (KEVM / yellow-paper model) is used to ground them; validation occurs inside the same LLM-influenced loop.
  • domain assumption The symbolic abstraction σ=⟨pc,stk,mem,sto,gas,env⟩ with frame conditions preserves the behaviors relevant to the injected bugs
    Section III-C: equality-encoded state transitions and frame conditions assume the bit-vector/array model captures all bug-relevant semantics of the Rust handlers.
  • domain assumption The 95 injected mutations are genuine semantic deviations from intended EVM behavior, correctly labeled and family-assigned
    Section IV-B1: construction process (injection authorship, selection, balance across five families) is not described, so representativeness and correctness of ground truth are unverifiable.
  • ad hoc to paper GPT-4o has no training-data advantage on the specific mutated samples (pretraining leakage is controlled)
    Section IV-B1 guards retrieval-DB leakage by source-file identity and opcode unit, but says nothing about the LLM having memorized the underlying public zkEVM codebase, which could inflate detection of mutations.
  • standard math Z3's bit-vector, array, and integer reasoning is sound for the encoded queries
    Section II-B: standard SMT soundness assumption; the encoding must also be well-sorted for this to apply.
  • domain assumption The reference database D contains only models verified against correct semantics
    Section III-B: entries are added after passing syntax, sort, execution, and 'associated semantic obligations' — but those obligations are themselves the self-validated Φ, so D's correctness is circular.

pith-pipeline@v1.3.0-alltime-deepseek · 13658 in / 18292 out tokens · 187211 ms · 2026-08-01T11:42:15.673371+00:00 · methodology

0 comments
Cite this review

Pith. "Pith review of Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis." pith.science (2026). https://pith.science/paper/WEFAEV4O

@misc{pith2026260719795,
  author       = {Pith},
  title        = {Pith review of: Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WEFAEV4O}},
  note         = {Machine review of arXiv:2607.19795}
}
Share X Bluesky LinkedIn Reddit HN
read the original 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.

Figures

Figures reproduced from arXiv: 2607.19795 by Guoqiang Li, Jingyang Li, Ling-I Wu, Shichen Huang, Yi Jiang, Zhenghe Jiang.

Figure 1
Figure 1. Figure 1: Motivation of LLM-guided verification model synthesis. Existing approaches fail to translate Rust implementations into formal verification models [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Example of semantic-to-SMT synthesis. Given a Rust implementation of the SSTORE opcode, VeriSynth maps key semantic operations to precise [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Practical comparison between handwritten Rust tests and VeriSynth [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

28 extracted references · 6 linked inside Pith

  1. [1]

    Zero-knowledge rollups,

    Ethereum Foundation, “Zero-knowledge rollups,” https://ethereum.org/en/developers/docs/scaling/zk-rollups/, accessed: 2026-06-27

    2026

  2. [2]

    Ethereum: A secure decentralised generalised transaction ledger,

    G. Wood, “Ethereum: A secure decentralised generalised transaction ledger,” Ethereum Yellow Paper, 2014. [Online]. Available: https://ethereum.github.io/yellowpaper/paper.pdf

    2014

  3. [3]

    Making smart contracts smarter,

    L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making smart contracts smarter,” inProceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016, pp. 254–269

    2016

  4. [4]

    Securify: Practical security analysis of smart contracts,

    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

    2018

  5. [5]

    Zeus: Analyzing safety of smart contracts,

    S. Kalra, S. Goel, M. Dhawan, and S. Sharma, “Zeus: Analyzing safety of smart contracts,” inProceedings of the Network and Distributed System Security Symposium, 2018

    2018

  6. [6]

    Kevm: A complete formal semantics of the ethereum virtual machine,

    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,” inPro- ceedings of the 31st IEEE Computer Security Foundations Symposium, 2018, pp. 204–217

    2018

  7. [7]

    Z3: An efficient smt solver,

    L. de Moura and N. Bjørner, “Z3: An efficient smt solver,” inProceed- ings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008, pp. 337–340

    2008

  8. [8]

    The smt-lib standard: Version 2.0,

    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/

    2010

  9. [9]

    Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs,

    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

    2008

  10. [10]

    A tool for checking ansi-c programs,

    D. Kroening, E. Clarke, and F. Lerda, “A tool for checking ansi-c programs,” inProceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2004, pp. 168–176

    2004

  11. [11]

    Symbolic execution and program testing,

    J. C. King, “Symbolic execution and program testing,” inCommunica- tions of the ACM, vol. 19, no. 7, 1976, pp. 385–394

    1976

  12. [12]

    Dynamically discovering likely program invariants to support program evolution,

    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

    2001

  13. [13]

    Houdini, an annotation assistant for esc/java,

    C. Flanagan and K. R. M. Leino, “Houdini, an annotation assistant for esc/java,” inProceedings of the International Symposium of Formal Methods Europe, 2001, pp. 500–517

    2001

  14. [14]

    A survey of smart contract formal specification and verification,

    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

    Pith/arXiv arXiv 2008

  15. [15]

    An empirical analysis of vulnerability detection tools for solidity smart contracts using line level manually annotated vulnerabil- ities,

    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 vulnerabil- ities,”Empirical Software Engineering, vol. 31, no. 5, p. 143, 2026

    2026

  16. [16]

    Specgen: Automated generation of formal program specifications via large language models,

    L. Ma, S. Liu, Y . Li, X. Xie, and L. Bu, “Specgen: Automated generation of formal program specifications via large language models,” inProceedings of the 47th IEEE/ACM International Conference on Software Engineering, 2025

    2025

  17. [17]

    Propertygpt: Llm-driven formal verification of smart contracts through retrieval-augmented property generation,

    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

    Pith/arXiv arXiv 2024

  18. [18]

    Language models are few-shot learners,

    T. B. Brown, B. Mann, N. Ryder, M. Subbiah, J. Kaplan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askellet al., “Language models are few-shot learners,”Advances in Neural Information Processing Systems, vol. 33, pp. 1877–1901, 2020

    1901

  19. [19]

    A prompt pattern catalog to enhance prompt engineering with chatgpt,

    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,” inProceedings of the 30th Conference on Pattern Languages of Programs, 2023

    2023

  20. [20]

    Automated soundness and completeness vetting of polygon{zkEVM},

    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},” in34th USENIX Security Symposium (USENIX Security 25), 2025, pp. 4093–4108

    2025

  21. [22]

    Large language models for software engineering: A systematic literature review,

    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

    Pith/arXiv arXiv 2023

  22. [23]

    Conversational automated program repair,

    C. S. Xia and L. Zhang, “Conversational automated program repair,”arXiv preprint arXiv:2301.13246, 2023. [Online]. Available: https://arxiv.org/abs/2301.13246

    Pith/arXiv arXiv 2023

  23. [25]

    Evm- fuzz: Differential fuzz testing of ethereum virtual machine,

    Y . Fu, M. Ren, F. Ma, X. Yang, H. Shi, S. Li, and X. Liao, “Evm- fuzz: Differential fuzz testing of ethereum virtual machine,”Journal of Software: Evolution and Process, vol. 36, no. 4, p. e2556, 2024

    2024

  24. [26]

    Training language models to follow instructions with human feedback,

    L. Ouyang, J. Wu, X. Jiang, D. Almeida, C. Wainwright, P. Mishkin, C. Zhang, S. Agarwal, K. Slama, A. Rayet al., “Training language models to follow instructions with human feedback,” inAdvances in Neural Information Processing Systems, 2022, pp. 27 730–27 744

    2022

  25. [27]

    Chain-of-thought prompting elicits reasoning in large language models,

    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,” inAdvances in Neural Information Processing Systems, 2022, pp. 24 824–24 837

    2022

  26. [28]

    Self-consistency improves chain of thought reasoning in language models,

    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,” inProceedings of the Inter- national Conference on Learning Representations, 2023

    2023

  27. [2021]

    Available: https://arxiv.org/abs/2107.03374

    [Online]. Available: https://arxiv.org/abs/2107.03374

    Pith/arXiv arXiv

  28. [2023]

    Available: https://arxiv.org/abs/2303.08774

    [Online]. Available: https://arxiv.org/abs/2303.08774

    Pith/arXiv arXiv