Pith. sign in

REVIEW 5 major objections 5 minor 1 cited by

Supporting Software Formal Verification with Large Language Models: An Experimental Study

T0 review · 5 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read Pairing Claude 3.5 Sonnet with the ESBMC verifier turns natural-language requirements into checkable properties, matches CoCoSim's 46.5% rate, and catches a floating-point bug CoCoSim missed.

desk verdict A credible end-to-end LLM-to-ESBMC experiment on the LMCPS benchmark with a real floating-point bug, but the FP/FN comparison to CoCoSim rests on a manual, unblinded equivalence classification that the paper itself concedes is lossy. read the letter →

arxiv 2507.04857 v1 pith:SBNE4UGT submitted 2025-07-07 cs.SE

Weiqi Wang , Marie Farrell , Lucas C. Cordeiro , Liping Zhao This is my paper · ORCID
classification cs.SE
keywords largelanguagemodelsformalverificationrequirementsengineeringboundedmodelcheckingESBMCCoSimcyber-physicalsystemsfloating-pointprecision
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper tries to establish that a large language model can take over the manual steps of formal software verification: turning plain-English requirements into machine-checkable properties. The authors build SpecVerify, a pipeline in which Claude 3.5 Sonnet converts a natural-language requirement plus its C implementation into C assertions, and the ESBMC bounded model checker verifies them. On nine Lockheed Martin cyber-physical systems (the LMCPS benchmark), the pipeline completes verification on 46.5% of properties—the same rate as NASA's CoCoSim—while reporting zero false positives and two false negatives versus CoCoSim's two and six. It also expresses requirements that linear temporal logic cannot (previous states, event counts) and finds a genuine floating-point median bug that CoCoSim missed because it used rational arithmetic. If these results hold, LLMs meaningfully lower the expertise barrier to formal verification, with requirement-document quality and human monitoring still deciding the outcome.

What carries the argument

The load-bearing mechanism is a two-stage LLM workflow. In stage one, the LLM reads the natural-language requirement together with the C code and emits a formalized requirement specification (a human-readable intermediate document), a role the paper maps to FRET. In stage two, the same LLM turns that specification into C assertions—including auxiliary variables that record previous states, counters, and boundary conditions—which ESBMC v7.7 checks against the code by bounded model checking, a role the paper maps to CoCoSim. The comparison apparatus rests on a Hoare-style triple (precondition, function, postcondition) used to judge whether LLM-generated assertions are logically equivalent to manually written ones.

What would settle it

Run the same 58 properties through a second C verifier such as CBMC with the same generated assertions, and have two independent blinded reviewers redo the logic-equivalence rating; if the false-positive and false-negative counts (0 and 2 for the LLM pipeline versus 2 and 6 for CoCoSim) do not reproduce, the comparison collapses. Separately, compile the triplex-monitor median code, evaluate it in single-precision IEEE 754 arithmetic on the inputs a=1.813356e+24, b=2.328307e-10, and c=1.999512, and confirm that the program selects b rather than the true median c.

Watch

Extended reading notes

Core claim

The paper's central claim is that SpecVerify—an automated pipeline pairing the Claude 3.5 Sonnet language model with the ESBMC bounded model checker—can take a natural-language requirement and the corresponding C code and produce verification properties that a formal verifier can run automatically, replacing the manual formalization work that tools like FRET and CoCoSim still require. Evaluated on nine of the ten Lockheed Martin Cyber-Physical Systems (LMCPS) tasks, the pipeline verifies 27 of 58 properties (46.5%), matching NASA's CoCoSim rate, with zero false positives and two false negatives compared with CoCoSim's two and six. The paper further claims that 79.31% of the generated assertions are logically equivalent to the human-written reference properties, that the pipeline can express requirements beyond LTL (previous-state references, event counters) through automatically generated auxiliary variables, and that ESBMC's floating-point semantics let it catch a median-computation bug in the triplex signal monitor that CoCoSim missed precisely because it reasoned with exact rational arithmetic.

Load-bearing premise

The entire comparison against CoCoSim rests on the authors' own manual judgment that the LLM-generated assertions mean the same thing as the human-written properties, and the paper itself admits that this judgment uses a simplified representation and is open to subjective bias.

Editorial extensions

If this is right

  • Domain experts who cannot write temporal logic can still obtain verification properties: the pipeline converts natural-language requirements plus C code into ESBMC-checkable assertions automatically.
  • On the nine LMCPS systems the pipeline verifies 27 of 58 properties (46.5%), the same rate as CoCoSim, with zero false positives and two false negatives versus two and six.
  • Verification scenarios LTL cannot express—previous-state references, event counting, multi-variable interactions—become expressible because the LLM writes C assertions with auxiliary variables.
  • Floating-point verification semantics expose numerical errors that rational-arithmetic verification hides; the median bug in the triplex signal monitor is a concrete instance.
  • The pipeline still depends on requirement-document quality and human review, since ambiguous requirements produced misinterpretations in both Claude and ChatGPT runs.
  • Different model choices change outcomes dramatically: ChatGPT 4o1 managed only a 25.9% verification rate with 23 assertion errors, while Llama 3.1 8B could not complete any task.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same two-stage prompt-and-verify recipe could be re-run against other C-level verifiers (for example, CBMC or Frama-C) on the same 58 properties; whether the zero-false-positive result is specific to ESBMC's floating-point semantics is directly testable.
  • Because the intermediate formal specification surfaces interpretation issues before verification, inserting a human checkpoint between the two phases would likely recover most of the 3.45% misunderstanding and 3.45% missing-assumption cases at modest cost.
  • The floating-point median finding suggests LLM-generated assertions can serve as a practical differential oracle: run the same requirement under different arithmetic semantics (float versus rational) to flag numerical bugs in auto-generated control code.
  • If the manual equivalence judgment is replaced by an automated criterion (for example, comparing counterexample sets), the 79.31% equivalence result could be made repeatable across other benchmarks.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 5 minor

Summary. This paper presents SpecVerify, a two-stage pipeline in which an LLM (Claude 3.5 Sonnet) translates natural-language requirements and Simulink-generated C code into a semi-formal specification and then into C assertions, which are checked with ESBMC. The evaluation covers nine tasks from the Lockheed Martin LMCPS benchmark (58 requirements) and compares against published FRET/CoCoSim and Simulink Design Verifier results. The headline findings are a 46.5% verification rate, comparable to CoCoSim, with zero false positives and two false negatives for Claude+ESBMC (versus two and six for CoCoSim), plus the discovery of a floating-point median-calculation error that CoCoSim missed because it used rational arithmetic. The paper also reports an RQ1 analysis claiming full automation and 79.31% logical equivalence between LLM-generated assertions and human-written properties, and an RQ2 comparison with detailed case studies.

Significance. If validated, the contribution is practically significant: the paper demonstrates a plausible end-to-end path from natural-language requirements to bounded-model-checking assertions, addresses expressiveness limitations of LTL-based workflows by generating auxiliary variables, and releases a public benchmark artifact. The floating-point median bug is a concrete, falsifiable finding supported by a numeric IEEE-754 derivation and a test case. However, the significance is contingent on the reliability of the manual logic-equivalence classification, which underpins the false-positive/false-negative comparison with CoCoSim, and on the counting conventions in Table V. The small size of the Simulink-generated codebase and the exclusion of a local-model baseline limit generalization, but the paper explicitly acknowledges these limitations.

major comments (5)
  1. [§IV.E.2, Table III] The head-to-head comparison with CoCoSim rests on the classification in Table III, but that classification is produced by an unblinded manual review using a simplified precondition-function-postcondition triple, and Section VI.4 concedes that this representation 'may oversimplify the complex logical relationships' and that human evaluators introduce 'subjective bias.' No inter-rater reliability, blind protocol, or mechanized equivalence check is reported. Since the 46 'Logic Equivalent' assertions are the basis for counting ESBMC-decided cases as requirement satisfactions in Table V, the 0-vs-2 false-positive and 2-vs-6 false-negative claims are not yet established. Please provide the full assertion-to-requirement mapping, a second independent annotation, and/or a mechanical check such as vacuity checks, assertion-strengthening checks, or refinement in a suitable logic.
  2. [Table V and footnote] The Table V footnote counts CoCoSim's 'FN-Unknown due to sin/cos solver error' as false negatives, which conflates an incomplete solver outcome ('unknown') with a wrong 'safe' verdict. The claimed difference of six false negatives is therefore not a straightforward accuracy comparison. Please report unknown or incomplete solver results separately and justify why solver incompleteness is counted as a false negative; otherwise the comparison overstates SpecVerify's advantage.
  3. [§V.B, Eqs. (1)–(8)] The floating-point median bug is reported with a concrete numeric derivation, but the text does not state whether the LLM-generated assertion alone caused ESBMC to find this bug, or whether the counterexample was found through the authors' post-hoc manual analysis described in Section IV.C. If the latter, this finding does not directly support the automation claim. Please clarify the provenance of the finding, include the exact assertion, and report the ESBMC output that exposed the bug.
  4. [§IV.D, Table I, Table V] The aggregate verification-rate comparison is muddled by inconsistent denominators. Table V reports 'Verified/Formed/Total' as 27/54/58 for CoCoSim, 21/54/58 for SLDV, 27/58/58 for Claude+ESBMC, and 15/35/58 for ChatGPT+ESBMC, while the verification-rate row uses 58 as the base for all tools. Because four requirements were not formable in CoCoSim/SLDV and one benchmark task was removed, the 46.5% for CoCoSim and the 46.5% for Claude are not directly comparable unless the same base (all 58, or all successfully formed) is used and the unformable requirements are treated uniformly. Please report both total-based and formed-based rates and clarify how unformed and skipped requirements enter the false-positive and false-negative counts.
  5. [§VI.3 and §IV.E.2] The paper acknowledges that 'the contributions of LLMs and ESBMC are mixed' and that 'considerable manual work is required' to verify the code generated by Claude, yet the RQ1 answer claims 'full automation in transforming natural language requirements into formal verification properties.' These statements are in tension. Please define the level of automation precisely, distinguishing the automated pipeline from the manual validation steps used to produce the evaluation, and report how much human effort was actually required for the 58-requirement benchmark.
minor comments (5)
  1. [Abstract and throughout] There are typesetting irregularities such as 'SpecV erify' and 'V erify' in the abstract and index terms; also, 'FRETish' is capitalized inconsistently as 'FRETISH' in Section II. Please correct these.
  2. [§II.A.2, Table V] The acronym 'SLDV' is used without definition; it should be introduced as Simulink Design Verifier at first use.
  3. [Table V footnote] The footnote for ChatGPT+ESBMC says 'FP includes FN-Unknown due to non-det input setup assertion'; this appears to misname false negatives as false positives and is confusing. Please rephrase the footnote to distinguish the two categories.
  4. [Figure 2] The Venn diagrams in Figure 2 have no legend or textual explanation of the numbers in each region; the text refers to 'two extra errors' but the figure is not interpretable without a key. Please add a caption or explanation.
  5. [§IV.D] The exact prompts and model parameters used for Claude 3.5 Sonnet and ChatGPT are not reported; for reproducibility, please provide the prompt templates, temperature settings, and API access dates in an appendix or repository file.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the headline 46.5% verification rate is a raw ESBMC outcome on the external LMCPS benchmark, not a fitted or self-referential quantity.

full rationale

The paper's central claims are empirical measurements rather than derivations from fitted parameters. The 46.5% completion rate is computed in Table V as Verified/Total (27/58) for Claude+ESBMC, where the verified count is produced by running the independent ESBMC model checker on LLM-generated C assertions over the externally published Lockheed Martin LMCPS benchmark. The comparison to CoCoSim is likewise anchored outside the paper: CoCoSim results are taken from the LMCPS challenge literature, and disputed counterexamples are checked by executing generated test witnesses. The manual 'logic equivalence' review in Section IV.E.2 and Table III is a real validity threat, since it is unblinded and the paper itself concedes possible oversimplification and subjective bias in Section VI.4. However, that review is not circular in the technical sense: the equivalence labels are evaluative judgments about the LLM's assertion-generation quality, not quantities that are mathematically forced by the definition of the verification rate or by a fitted model. No equation in the paper reduces to another by construction, no fitted parameter is renamed as a prediction, and no load-bearing premise is justified solely by a self-citation chain. The authors' prior citations, such as the FRET case studies, are background support rather than the basis of the main result. ESBMC's provenance includes a co-author, but ESBMC is an externally maintained and widely used verifier, so using it does not make the evaluation circular. Overall, the derivation chain is empirically self-contained with respect to an external benchmark and an independent verification tool.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No free parameters are fitted; the study has no numerical model to calibrate. The axioms are the standard trust assumptions of empirical verification research: tool correctness, benchmark ground truth, and the validity of the authors' manual equivalence judgment. The manual equivalence judgment is the most fragile, as Section VI.4 concedes that the 3-tuple representation may oversimplify complex logical properties.

assumptions (4)
  • domain assumption ESBMC's bounded model checking with floating-point semantics is a sound oracle for the generated C code under the checked bounds.
    The study treats ESBMC verdicts on generated assertions as ground truth for error classification (Section IV.D, V.B).
  • domain assumption The LMCPS benchmark requirements and the CoCoSim/SLDV baseline results from prior publications are accurate ground truth except where independently corrected.
    Table V and the RQ2 comparisons assume the previously published baseline results are trustworthy enough for comparison (Section IV.C).
  • domain assumption The authors' manual logic-equivalence review using precondition-function-postcondition triples is a valid measure of equivalence between LLM-generated and human-written properties.
    The 79.31% equivalence figure and false positive/false negative counts depend on this manual judgment (Section IV.E.2, VI.4).
  • domain assumption Embedded Coder's C translation faithfully reflects the Simulink model semantics for the nine systems.
    The pipeline verifies the generated C, but the requirements refer to the Simulink models; any translation bugs would affect all comparisons (Section IV.B).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Supporting Software Formal Verification with Large Language Models: An Experimental Study." pith.science (2026). https://pith.science/paper/SBNE4UGT

@misc{pith2026250704857,
  author       = {Pith},
  title        = {Pith review of: Supporting Software Formal Verification with Large Language Models: An Experimental Study},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SBNE4UGT}},
  note         = {Machine review of arXiv:2507.04857}
}
read the original abstract

Formal methods have been employed for requirements verification for a long time. However, it is difficult to automatically derive properties from natural language requirements. SpecVerify addresses this challenge by integrating large language models (LLMs) with formal verification tools, providing a more flexible mechanism for expressing requirements. This framework combines Claude 3.5 Sonnet with the ESBMC verifier to form an automated workflow. Evaluated on nine cyber-physical systems from Lockheed Martin, SpecVerify achieves 46.5% verification accuracy, comparable to NASA's CoCoSim, but with lower false positives. Our framework formulates assertions that extend beyond the expressive power of LTL and identifies falsifiable cases that are missed by more traditional methods. Counterexample analysis reveals CoCoSim's limitations stemming from model connection errors and numerical approximation issues. While SpecVerify advances verification automation, our comparative study of Claude, ChatGPT, and Llama shows that high-quality requirements documentation and human monitoring remain critical, as models occasionally misinterpret specifications. Our results demonstrate that LLMs can significantly reduce the barriers to formal verification, while highlighting the continued importance of human-machine collaboration in achieving optimal results.

Figures

Figures reproduced from arXiv: 2507.04857 by the authors.

Figure 1
Figure 1. Proposed Approach: Software Verification Process Supported by LLMs. LLMs guide formal specification and property [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Venn Diagrams comparing verification results [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. The 4/$\delta$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee

    cs.AI 2025-11 reject novelty 2.0 of 10

    The 4/δ bound is the mean of four geometric distributions, not a new theorem, and the simulation validation is circular.

Reference graph

Works this paper leans on

35 extracted references · 26 canonical work pages · cited by 1 Pith paper

  1. [1]

    Cbmc–c bounded model checker: (competition contribution),

    D. Kroening and M. Tautschnig, “Cbmc–c bounded model checker: (competition contribution),” inTools and Algorithms for the Construc- tion and Analysis of Systems: 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings 20. Sprin...

    work page 2014

  2. [2]

    Esbmc 5.0: an industrial-strength c model checker,

    M. R. Gadelha, F. R. Monteiro, J. Morse, L. C. Cordeiro, B. Fischer, and D. A. Nicole, “Esbmc 5.0: an industrial-strength c model checker,” inProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018, pp. 888–891

    work page 2018

  3. [3]

    Nusmv: A new symbolic model verifier,

    A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, “Nusmv: A new symbolic model verifier,” inComputer Aided Verification: 11th Interna- tional Conference, CAV’99 Trento, Italy, July 6–10, 1999 Proceedings

    work page 1999

  4. [4]

    The model checker spin,

    G. J. Holzmann, “The model checker spin,”IEEE Transactions on software engineering, vol. 23, no. 5, pp. 279–295, 1997

    work page 1997

  5. [5]

    Formal methods: Practice and experience,

    J. Woodcock, P. G. Larsen, J. Bicarregui, and J. Fitzgerald, “Formal methods: Practice and experience,”ACM computing surveys (CSUR), vol. 41, no. 4, pp. 1–36, 2009

    2009

  6. [6]

    Gpt-4 technical report,

    J. Achiam, S. Adler, S. Agarwal, L. Ahmad, I. Akkaya, F. L. Aleman, D. Almeida, J. Altenschmidt, S. Altman, S. Anadkatet al., “Gpt-4 technical report,”arXiv preprint arXiv:2303.08774, 2023

    arXiv 2023

  7. [7]

    Tr2mtl: Llm based frame- work for metric temporal logic formalization of traffic rules,

    K. Manas, S. Zwicklbauer, and A. Paschke, “Tr2mtl: Llm based frame- work for metric temporal logic formalization of traffic rules,” in2024 IEEE Intelligent Vehicles Symposium (IV). IEEE, 2024, pp. 1206–1213

    work page 2024

  8. [8]

    nl2spec: Interactively translating unstructured natural language to temporal logics with large language models,

    M. Cosler, C. Hahn, D. Mendoza, F. Schmitt, and C. Trippel, “nl2spec: Interactively translating unstructured natural language to temporal logics with large language models,” inInternational Conference on Computer Aided Verification. Springer, 2023, pp. 383–396

    work page 2023

Show all 35 references
  1. [9]

    Assertllm: Generating hardware verification assertions from design specifications via multi-llms,

    Z. Yan, W. Fang, M. Li, M. Li, S. Liu, Z. Xie, and H. Zhang, “Assertllm: Generating hardware verification assertions from design specifications via multi-llms,” inProceedings of the 30th Asia and South Pacific Design Automation Conference, 2025, pp. 614–621

    2025

  2. [10]

    Advancing theorem proving in llms through large-scale synthetic data,

    H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang, “Advancing theorem proving in llms through large-scale synthetic data,” inThe 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024

    2024

  3. [11]

    Springer, 1999, pp. 495–499

    1999

  4. [12]

    Co- cosim, a code generation framework for control/command applications: An overview of cocosim for multi-periodic discrete simulink models,

    H. Bourbouh, P.-L. Garoche, T. Loquen, É. Noulard, and C. Pagetti, “Co- cosim, a code generation framework for control/command applications: An overview of cocosim for multi-periodic discrete simulink models,” Embedded Real Time Systems (ERTS) 2020, no. ARC-E-DAA-TN74591, 2020

    2020

  5. [13]

    Formal requirements elicitation with fret,

    D. Giannakopoulou, A. Mavridou, J. Rhein, T. Pressburger, J. Schumann, and N. Shi, “Formal requirements elicitation with fret,” inInternational Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-2020), no. ARC-E-DAA-TN77785, 2020

    2020

  6. [14]

    The ten lockheed martin cyber- physical challenges: formalized, analyzed, and explained,

    A. Mavridou, H. Bourbouh, D. Giannakopoulou, T. Pressburger, M. He- jase, P.-L. Garoche, and J. Schumann, “The ten lockheed martin cyber- physical challenges: formalized, analyzed, and explained,” in2020 IEEE 28th International Requirements Engineering Conference (RE). IEEE, 2...

    2020

  7. [15]

    (2024, 10) Claude 3.5 sonnet

    Anthropic. (2024, 10) Claude 3.5 sonnet. [Online]. Available: https://www.anthropic.com/news/claude-3-5-sonnet

    2024

  8. [16]

    (n.d.) Using openai o1 models and gpt-4o models on chatgpt

    OpenAI. (n.d.) Using openai o1 models and gpt-4o models on chatgpt. Accessed: 2025-02-

    2025

  9. [17]

    An automata-theoretic approach to linear temporal logic,

    M. Y . Vardi, “An automata-theoretic approach to linear temporal logic,” Logics for concurrency: structure versus automata, pp. 238–266, 2005

    2005

  10. [18]

    Automated translation of natural language requirements to runtime monitors,

    I. Perez, A. Mavridou, T. Pressburger, A. Goodloe, and D. Gian- nakopoulou, “Automated translation of natural language requirements to runtime monitors,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2022, pp. 387– 395

    2022

  11. [19]

    Fretting and formal modelling: a mechanical lung ventilator,

    M. Farrell, M. Luckcuck, R. Monahan, C. Reynolds, and O. Sheridan, “Fretting and formal modelling: a mechanical lung ventilator,” inInter- national Conference on Rigorous State-Based Methods. Springer, 2024, pp. 360–383

    2024

  12. [20]

    The kind 2 model checker,

    A. Champion, A. Mebsout, C. Sticksel, and C. Tinelli, “The kind 2 model checker,” inInternational Conference on Computer Aided Verification. Springer, 2016, pp. 510–517

    2016

  13. [21]

    Integration and evaluation of the advocate, fret, cocosim, and event-b tools on the inspection rover case study,

    H. Bourbouh, M. Farrell, A. Mavridou, and I. Sljivo, “Integration and evaluation of the advocate, fret, cocosim, and event-b tools on the inspection rover case study,” NASA, Tech. Rep., 2020

    2020

  14. [22]

    Verifying plc programs via monitors: Extending the integration of fret and plcverif,

    X. Fink, A. Mavridou, A. Katis, and B. F. Adiego, “Verifying plc programs via monitors: Extending the integration of fret and plcverif,” inNASA Formal Methods Symposium. Springer, 2024, pp. 427–435

    2024

  15. [23]

    Enchanting program specification synthesis by large language models using static analysis and program verification,

    C. Wen, J. Cao, J. Su, Z. Xu, S. Qin, M. He, H. Li, S.-C. Cheung, and C. Tian, “Enchanting program specification synthesis by large language models using static analysis and program verification,” inInternational Conference on Computer Aided Verification. Springer, 2024, pp. 302– 328

    2024

  16. [24]

    Available: https://help.openai.com/en/articles/ 9824965-using-openai-o1-models-and-gpt-4o-models-on-chatgpt

    [Online]. Available: https://help.openai.com/en/articles/ 9824965-using-openai-o1-models-and-gpt-4o-models-on-chatgpt

  17. [25]

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

    Y . Liu, Y . Xue, D. Wu, Y . Sun, Y . Li, M. Shi, and Y . Liu, “Propertygpt: Llm-driven formal verification of smart contracts through retrieval- augmented property generation,” inProceedings of the Network and Distributed System Security Symposium, San Diego, CA, USA, February 2025

    2025

  18. [26]

    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,”arXiv preprint arXiv:2401.08807, 2024

    2024 arXiv

  19. [27]

    Can large language models transform natural language intent into formal method postconditions?

    M. Endres, S. Fakhoury, S. Chakraborty, and S. K. Lahiri, “Can large language models transform natural language intent into formal method postconditions?”Proceedings of the ACM on Software Engineering, vol. 1, no. FSE, pp. 1889–1912, 2024

    1912

  20. [28]

    Verilogreader: Llm-aided hardware test generation,

    R. Ma, Y . Yang, Z. Liu, J. Zhang, M. Li, J. Huang, and G. Luo, “Verilogreader: Llm-aided hardware test generation,” in2024 IEEE LLM Aided Design Workshop (LAD). IEEE, 2024, pp. 1–5

    2024

  21. [29]

    Fveval: Un- derstanding language model capabilities in formal verification of digital hardware,

    M. Kang, M. Liu, G. B. Hamad, S. M. Suhaib, and H. Ren, “Fveval: Un- derstanding language model capabilities in formal verification of digital hardware,” in2025 Design, Automation & Test in Europe Conference (DATE). IEEE, 2025, pp. 1–6

    2025

  22. [30]

    Evaluating large language models trained on code,

    M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. D. O. Pinto, J. Kaplan, H. Edwards, Y . Burda, N. Joseph, G. Brockmanet al., “Evaluating large language models trained on code,”arXiv preprint arXiv:2107.03374, 2021

    2021 arXiv

  23. [31]

    Swe-bench: Can language models resolve real-world github issues?

    C. E. Jimenez, J. Yang, A. Wettig, S. Yao, K. Pei, O. Press, and K. Narasimhan, “Swe-bench: Can language models resolve real-world github issues?”arXiv preprint arXiv:2310.06770, 2023

    2023 arXiv

  24. [32]

    Aider leaderboard,

    Aider.AI, “Aider leaderboard,” https://aider.chat/, accessed: February 19, 2025

    2025

  25. [33]

    Llama 3.1-8b,

    I. Meta Platforms, “Llama 3.1-8b,” Hugging Face, 2024, accessed: 2025-02-02. [Online]. Available: https://huggingface.co/meta-llama/ Llama-3.1-8B

    2024

  26. [34]

    Semantical considerations on floyd-hoare logic,

    V . R. Pratt, “Semantical considerations on floyd-hoare logic,” in17th Annual Symposium on Foundations of Computer Science (sfcs 1976). IEEE, 1976, pp. 109–121

    1976

  27. [35]

    Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning,

    D. Guo, D. Yang, H. Zhang, J. Song, R. Zhang, R. Xu, Q. Zhu, S. Ma, P. Wang, X. Biet al., “Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning,”arXiv preprint arXiv:2501.12948, 2025

    2025 arXiv

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.