Pith. sign in

REVIEW 1 major objections 75 references

Automated Lemma Discovery in Agentic Program Verification

T0 review · 1 major / 0 minor · reviewed 2026-08-02 · deepseek-v4-flash

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

Pith's one-line read A proof agent that reads the source code before attacking the verification condition can discharge obligations that defeat state-of-the-art theorem-proving agents.

desk verdict Real advance on a real bottleneck; soundness claim needs a closure check and the evaluation needs artifacts, but the core idea is solid. read the letter →

arxiv 2603.22114 v2 pith:ROO3MG54 submitted 2026-03-23 cs.SE

Huan Zhao , Haoxin Tu , Zhengyao Liu , Martin C. Rinard , Abhik Roychoudhury This is my paper
classification cs.SE
keywords deductiveverificationLLMagentshelperlemmadiscoveryprogramcomprehensionproofautomationconditionsRocq/Coq
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

The paper claims that the bottleneck in automated deductive verification is not mathematical reasoning but the loss of program semantics inside tool-generated verification conditions, and that this bottleneck can be broken by discovering helper lemmas. LemmaNet first has an LLM analyze the annotated source and write a compact, source-level 'semantics-aware' proof obligation; it then synthesizes bridging lemmas that connect that obligation to the verbose proof-targeted VC emitted by a trusted VC generator. During proof search, an online adapter strengthens or rewrites these lemmas from the prover's feedback. Across 941 real-world verification conditions from standard and large-scale C benchmarks, LemmaNet proves 364 VCs, beating two state-of-the-art LLM proof agents by 26.8% and 51.7%. The approach is sound by design: every helper lemma is checked in the Rocq proof assistant and the final proof still discharges the trusted generator's obligation.

What carries the argument

Two-stage helper lemma discovery. Offline, a program semantic analyzer converts annotated source and specs into a compact semantics-aware theorem, and an obligation-aligned synthesizer produces lemmas that bridge that theorem to the proof-targeted VC. Online, an adaptive lemma maintainer holds the lemma library while feedback-guided adaptation refines lemmas when they fail in the evolving proof state. The load-bearing connection is the bridge between the two representations: lemmas such as 'shifting an address preserves the base' let the verbose, memory-model-laden VC be discharged by reusing the compact semantic proof.

What would settle it

Run LemmaNet and the baseline agents on a held-out set of C programs whose verification conditions were created after the model's training cutoff; if the proved-VC advantage drops to near zero, the reported improvements are an artifact of training-data overlap rather than of program-comprehension-driven lemma discovery.

Watch

Extended reading notes

Core claim

The paper claims that helper lemmas—auxiliary facts proved alongside the main obligation—are the missing ingredient in LLM-based verification of real C code, and that they can be discovered by analyzing the program source rather than the verbose verification condition alone. LemmaNet first builds a compact, source-level semantics-aware VC, proves it in Rocq, then asks the LLM to compare this with the proof-targeted VC emitted by Frama-C and synthesize bridging lemmas. As the proof unfolds, an online adapter refines those lemmas in response to prover feedback, by strengthening statements or revising conflicting representations. Because the final proof still discharges the trusted VC generator

Load-bearing premise

The measured advantage rests on the assumption that the closed LLM has not memorized the benchmark programs and their verification conditions in a way that conveniently supplies the helper lemmas.

Editorial extensions

If this is right

  • VC proving agents gain a capability they previously lacked—inventing helper lemmas—which lets automated verification scale to larger, real-world C programs.
  • Soundness does not depend on the LLM: since the final proof targets the trusted VC and all lemmas are machine-checked, arbitrary LLM errors cannot produce a false certificate.
  • Both discovery stages matter: disabling online adaptation drops proved VCs from 364 to 302, disabling offline synthesis drops them to 328, and removing program semantic analysis drops them to 301.
  • The dominant proof strategy is bridging tool-specific encodings to program-level semantics (88% of unique helper-lemma proofs), suggesting semantic mismatch is a main obstacle in VC proving.
  • Per-VC API costs of roughly $0.36 in the proving phase mean the gain is obtainable at modest expense.

Reading between the lines

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

  • If the measured advantage were re-run with a fully open model or with programs released after the model's cutoff, the 26.8%–51.7% gap might shrink; the absence of an auditable training corpus makes this the key open question about the benchmark evidence.
  • The same two-obligation design could transfer to other verification toolchains and proof assistants, since the trick is generic: compare a source-level proof with a tool-generated one and bridge them.
  • A testable extension is to replace the formal semantics-aware VC with a natural-language hint of the program's key invariant; if gains persist, the essential ingredient is semantic guidance rather than the formal bridge theorem.
  • Robustness to tool changes could be probed by regenerating VCs with a different version of the VC generator and checking whether offline lemmas remain applicable; high reuse would show the lemmas capture program semantics, not tool quirks.
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

1 major / 0 minor

Summary. The paper proposes LemmaNet, an LLM-based proof agent for discharging verification conditions (VCs) extracted from C programs by Frama-C and proved in Rocq. LemmaNet extends an existing tactic-by-tactic agent, AutoRocq, with two new mechanisms: (1) an offline lemma synthesizer that uses an LLM to construct a 'semantics-aware VC' from the annotated source code and then generates helper lemmas bridging that VC to the verbose proof-targeted VC produced by Frama-C's WP plugin; and (2) an online lemma adapter that maintains a library of helper lemmas and refines them in response to proof-assistant feedback. The system is evaluated on 941 VCs from SV-COMP and NTP4VC, reporting 364 successes versus 287 for AutoRocq and 240 for Copra, with ablations showing that the offline synthesizer, online adapter, and program semantic analyzer each contribute. The paper also presents a taxonomy of helper-lemma utility and two case studies.

Significance. If the result holds, the paper addresses a real bottleneck in deductive verification: existing LLM proof agents do not discover helper lemmas, and the paper's program-comprehension-based framing is a plausible and useful contribution. The architecture has credible strengths: final proof terms are checked by Rocq, helper lemmas are intended to come with formal proofs, the offline/online distinction is clearly described, and the evaluation uses external benchmarks with ablations and case studies. However, the central soundness claim is not yet established: the implementation does not verify that generated helper-lemma proofs are closed under axioms, so 'sound by design' is only as strong as an unstated axiom-closure check. The empirical magnitude is also weakened by the acknowledged data-leakage risk, the absence of an artifact, and reliance on a single unverifiable run against a closed API model. The paper is worth pursuing, but the soundness machinery must be made explicit and the evaluation made reproducible before the claims can be accepted.

major comments (1)
  1. [§4.4 and §6] The paper's soundness claim ('the TCB includes only the Rocq and Frama-C kernels... soundness guarantees hold in the face of arbitrary LLM behavior') is not supported by the implementation description. Section 4.4 says the offline synthesizer 'checks its output in the Rocq proof assistant,' and Section 6 says all dependent helper lemmas are 'formally stated and machine-checked in Rocq.' In Rocq, a file containing `Admitted` (or a top-level `admit`) compiles successfully and introduces a global axiom; `Qed` on the final theorem does not prevent the theorem from depending on that axiom. The manuscript never states that generated helper-lemma proofs are axiom-free (e.g., via `Print Assumptions` returning nil or an equivalent fail-on-admit flag). Without such a check, a hallucinating or adversarial LLM can inject an unproven helper lemma, and the 'sound by design' statement collapses. If any

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: gains are measured on external benchmarks and helper lemmas are checked by Rocq; the AutoRocq self-citation is not load-bearing.

full rationale

The derivation chain is not circular. LemmaNet's central claim—that offline semantics-aware lemma synthesis plus online adaptation improves VC proving—is evaluated by running the full system and ablations on 941 VCs from SV-COMP and NTP4VC, with all tools using the same backend LLM and temperature 0 (Sec. 5.1). The claimed 26.8%–51.7% improvements are computed from the observed proof counts in Table 1, not from any parameter fitted to those counts. The offline synthesizer's helper lemmas are generated by an LLM but the system "checks its output in the Rocq proof assistant" (Sec. 4.4), and the final proof discharges the trusted VC generator's proof-targeted VC; the semantics-aware VC is explicitly not treated as a soundness basis (Sec. 3, Key Insights). AutoRocq [61] is prior work by overlapping authors and is used both as base agent and baseline, but this is not load-bearing: the comparison is re-run in this paper, and ablations (¬Ofl, ¬Onl, ¬PSA) independently isolate the contributions. No step reduces to a fit, a definitional equivalence, an imported uniqueness theorem, or an ansatz smuggled in by citation. Two non-circular validity risks exist but do not affect the circularity verdict: (1) Sec. 6 admits "the benchmarks used in our evaluation may have been seen by the underlying LLM during training," though no ground-truth proofs are public; (2) Sec. 4.4's statement that the synthesizer checks output in Rocq does not explicitly rule out accepted 'Admitted' axioms, so the Sec. 6 claim that soundness holds "in the face of arbitrary LLM behavior" is under-supported. These are correctness/validity concerns, not circular reductions.

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

No numeric free parameters are fitted; this is an empirical systems paper. The central claims rest on toolchain trust, LLM capability assumptions, benchmark representativeness, and absence of data leakage, rather than on fitted constants or newly postulated entities.

assumptions (4)
  • domain assumption Frama-C's WP VC generator and the Rocq kernel are sound, so discharging the generated proof-targeted VC implies program correctness.
    Invoked in Section 4.4 and Section 6 (Soundness): the trusted computing base is stated to be the Rocq and Frama-C kernels, with the LLM outside the TCB.
  • domain assumption The LLM can, given source code/specifications and the provided prompts, produce valid Rocq helper lemma statements and proofs, or refine them online from proof-assistant feedback.
    The effectiveness of both the offline synthesizer (Section 4.2) and online adapter (Section 4.3) depends on this capability; the paper itself notes in Limitations that the offline synthesizer may fail for deep domain knowledge.
  • domain assumption The SV-COMP and NTP4VC benchmark VCs are representative of real-world verification conditions and are correctly extracted.
    Section 5.1 describes the benchmark sources and VC categories; the evaluation's external validity rests on this assumption.
  • domain assumption The closed LLM has not memorized the benchmark VCs or their proofs in a way that advantages LemmaNet disproportionately.
    Section 6 (Threats to Validity) lists data leakage as a potential threat and asserts it is minimal because no ground-truth proofs are public; with a closed model this cannot be verified.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Automated Lemma Discovery in Agentic Program Verification." pith.science (2026). https://pith.science/paper/ROO3MG54

@misc{pith2026260322114,
  author       = {Pith},
  title        = {Pith review of: Automated Lemma Discovery in Agentic Program Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ROO3MG54}},
  note         = {Machine review of arXiv:2603.22114}
}
read the original abstract

Deductive verification provides strong correctness guarantees for code by extracting verification conditions (VCs) and writing formal proofs for them. The expertise-intensive task of VC proving is the main bottleneck in this process, and has been partly automated owing to recent advances in Large Language Model (LLM) agents. However, existing proof agents are not able to discover helper lemmas -- auxiliary lemmas that aid in proving -- and thus fall short as programs grow in size and complexity. In this paper, we argue that VC proving for program verification is more than a purely mathematical task, and benefits considerably from program comprehension. Our key insight is that human proof engineers often discover and apply helper lemmas based on their understanding of the program semantics, which are not directly reflected in the VCs produced by VC generators. Inspired by this insight, we propose an LLM agent, LemmaNet, that discovers helper lemmas in two ways. Specifically, the agent first synthesizes lemmas offline by directly analyzing the source code and specifications and then relating this semantic understanding to the mechanical, verbose encoding produced by VC generators. As the proof unfolds, LemmaNet then adapts existing helper lemmas online to accommodate evolving proof states, enabling the agent to effectively discharge complex VCs on-the-fly. We implement LemmaNet on top of an existing proof agent AutoRocq for Rocq and the Frama-C ecosystem, and evaluate it on SV-COMP and established real-world subjects, including modules of the Linux kernel, Contiki OS, standard C++ library, and X.509 parser. Our experimental results demonstrate that LemmaNet significantly outperforms state-of-the-art approaches, highlighting the importance of program comprehension-aided lemma discovery in agentic program verification.

Figures

Figures reproduced from arXiv: 2603.22114 by the authors.

Figure 1
Figure 1. Source code of hex2bin.c with ACSL annotation and the loop invariant to prove being highlighted. 2.2 Theorem Proving for Verification Machine Learning for Proof Automation. Automating proof con￾struction is a key step toward closing the verification gap. Recent advances in machine learning have spurred numerous approaches to this problem. Pioneering efforts [52, 69] frame proof synthe￾sis as sequence prediction, emp… view at source ↗
Figure 2
Figure 2. (a) proof-targeted VC 𝜙𝐶 v/s (b) semantics-aware VC 𝜙𝐴 for the highlighted loop invariant in [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 4
Figure 4. Prompt for program semantic analyzer. noting that, instead of generating the obligation in a vacuum, we instruct the LLM to generate a complete file in Rocq, including the statement and its proof with all the supporting definitions. This is possible because the semantics-aware VC is expressed in terms of source-level concepts and is amenable to straightforward proof. In the example from [PITH_FULL_IMAGE:figures/ful… view at source ↗
Figures from the paper (6 more)
Figure 5
Figure 5. Figure 5: Prompt for obligation-aligned lemma synthesis. [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 6
Figure 6. Figure 6: Prompt for feedback-guided lemma adaptation. [PITH_FULL_IMAGE:figures/full_fig_p007_6.png]
Figure 7
Figure 7. Figure 7: Venn diagram of the number of lemmas proved by [PITH_FULL_IMAGE:figures/full_fig_p008_7.png]
Figure 8
Figure 8. Figure 8: The number of VCs proved by different tools: a [PITH_FULL_IMAGE:figures/full_fig_p008_8.png]
Figure 3
Figure 3. Figure 3: We include the third ablative variant, ¬PSA, to evaluate the effectiveness of program-guided offline lemma discovery. We evaluate each variant on the entire benchmark set of 941 VCs. The last section of [PITH_FULL_IMAGE:figures/full_fig_p008_3.png]
Figure 9
Figure 9. Figure 9: Cardinality of helper lemmas: # of offline/online [PITH_FULL_IMAGE:figures/full_fig_p009_9.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

75 extracted references · 2 linked inside Pith

  1. [1]

    José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, and Bárbara Vieira

  2. [2]

    Yoav Alon and Cristina David. 2025. Integrating Large Language Models and Reinforcement Learning for Non-Linear Reasoning.Proceedings of the ACM on Software Engineering2, FSE (2025), 957–977

    2025

  3. [3]

    Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al . 2022. cvc5: A versatile and industrial-strength SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 415–442

    2022

  4. [4]

    Dirk Beyer and Jan Strejček. 2025. Improvements in Software Verification and Witness Validation: SV-COMP 2025. InTools and Algorithms for the Construction and Analysis of Systems. Springer Nature Switzerland, Cham, 151–186

    2025

  5. [5]

    Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. 2020. The Tactician: A seamless, interactive tactic learner and prover for Coq. InInternational Conference on Intelligent Computer Mathematics. Springer, 271–277

    2020

  6. [6]

    Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. 2018. Ghosts for lists: a critical module of Contiki verified in Frama-C. InNASA Formal Methods Symposium. Springer, 37–53

    2018

  7. [7]

    Ana Brendel, Aishwarya Sivaraman, and Todd Millstein. 2025. Synthesizing Implication Lemmas for Interactive Theorem Proving.Proceedings of the ACM on Programming Languages9, OOPSLA2 (2025), 2254–2278

    2025

  8. [8]

    Yuriy Brun, Saikat Chakraborty, Claire Le Goues, Corina Păsăreanu, and Adish Singla. 2026. Automatically Engineering Trusted Software: A Research Roadmap. ACM Transactions on Software Engineering and Methodology(March 2026)

    2026

Show all 75 references
  1. [9]

    Jochen Burghardt, Jens Gerlach, and Timon Lapawczyk. 2015. ACSL by example. https://publica.fraunhofer.de/handle/publica/297476

    2015

  2. [10]

    Nuno Carvalho, Cristiano da Silva Sousa, Jorge Sousa Pinto, and Aaron Tomb

  3. [11]

    Projet Coq. 1996. The coq proof assistant-reference manual.INRIA Rocquencourt and ENS Lyon, version5 (1996), 7–1

    1996

  4. [12]

    Łukasz Czajka and Cezary Kaliszyk. 2018. Hammer for Coq: Automation for dependent type theory.Journal of Automated Reasoning61, 1 (2018), 423–453

    2018

  5. [13]

    Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340

    2008

  6. [14]

    Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. The Lean theorem prover (system description). InInternational Conference on Automated Deduction. Springer, 378–388

    2015

  7. [15]

    Google DeepMind. [n. d.]. AlphaProof. https://deepmind.google/discover/blog/ai- solves-imo-problems-at-silver-medal-level/

  8. [16]

    Maxime Dénès, Catalin Hritcu, Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C Pierce. 2014. QuickChick: Property-based testing for Coq. In The Coq Workshop, Vol. 125. 126

    2014

  9. [17]

    Yinlin Deng, Chunqiu Steven Xia, Chenyuan Yang, Shizhuo Dylan Zhang, Shu- jing Yang, and Lingming Zhang. 2024. Large Language Models are edge-case generators: Crafting unusual programs for fuzzing deep learning libraries. In Proceedings of the 46th IEEE/ACM international confe...

    2024

  10. [18]

    Josiah Dodds and Andrew W Appel. 2013. Mostly sound type system improves a foundational program verifier. InInternational Conference on Certified Programs and Proofs. Springer, 17–32

    2013

  11. [19]

    Arnaud Ebalard, Patricia Mouy, and Ryad Benadjila. 2019. Journey to a RTE-free X. 509 parser. InSymposium sur la sécurité des technologies de l’information et des communications (SSTIC 2019), Vol. 186. 1–30

    2019

  12. [20]

    Denis Efremov, Mikhail Mandrykin, and Alexey Khoroshilov. 2018. Deductive verification of unmodified Linux kernel library functions. InInternational Sym- posium on Leveraging Applications of Formal Methods. Springer, 216–234

    2018

  13. [21]

    Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K Lahiri

  14. [22]

    Angela Fan, Beliz Gokkaya, Mark Harman, Mitya Lyubarskiy, Shubho Sengupta, Shin Yoo, and Jie M Zhang. 2023. Large Language Models for Software Engineer- ing: Survey and Open Problems. In2023 IEEE/ACM International Conference on Software Engineering: Future of Software Engineer...

    2023

  15. [23]

    Emily First, Yuriy Brun, and Arjun Guha. 2020. TacTok: Semantics-aware proof synthesis.Proceedings of the ACM on Programming Languages4, OOPSLA (2020), 1–31

    2020

  16. [24]

    Rabe, Talia Ringer, and Yuriy Brun

    Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole- Proof Generation and Repair with Large Language Models. InProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering(2023-11...

    2023

  17. [25]

    Frama-C Developers. 2026. Weakest Precondition (WP) Plug-in in Frama-C. https://www.frama-c.com/fc-plugins/wp.html Accessed: 2026-03-23

    2026

  18. [26]

    Jinyao Guo, Chengpeng Wang, Xiangzhe Xu, Zian Su, and Xiangyu Zhang. 2026. RepoAudit: An Autonomous LLM-Agent for Repository-Level Code Auditing. In Forty-second International Conference on Machine Learning. 1–18. 11 Conference acronym ’XX, June 03–05, 2018, Woodstock, NY Huan...

    2026

  19. [27]

    Xinyi Hou, Yanjie Zhao, Yue Liu, Zhou Yang, Kailong Wang, Li Li, Xiapu Luo, David Lo, John Grundy, and Haoyu Wang. 2024. Large Language Models for Software Engineering: A systematic literature review.ACM Transactions on Software Engineering and Methodology33, 8 (2024), 1–79

    2024

  20. [28]

    Moa Johansson. 2019. Lemma discovery for induction: a survey. InInternational Conference on Intelligent Computer Mathematics. Springer, 125–139

    2019

  21. [29]

    Moa Johansson, Lucas Dixon, and Alan Bundy. 2011. Conjecture synthesis for inductive theories.Journal of Automated Reasoning47, 3 (2011), 251–289

    2011

  22. [30]

    Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2015. Frama-C: A software analysis perspective.Formal Aspects of Computing27, 3 (2015), 573–609

    2015

  23. [31]

    Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood

    Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel.. InProceedings of t...

    2009

  24. [32]

    Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, and Nadia Polikarpova. 2024. CCLemma: e-graph guided lemma discovery for inductive equational proofs.Proceedings of the ACM on Programming Languages8, ICFP (2024), 818–844

    2024

  25. [33]

    Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types (extended version).CoRRabs/2303.05491 (2023). https://doi.org/10.48550/arXiv.2303.05491

    2023 doi arXiv

  26. [34]

    Julia Lawall, Keisuke Nishimura, and Jean-Pierre Lozi. 2024. Should we balance? Towards formal verification of the Linux kernel scheduler. InInternational Static Analysis Symposium. Springer, 194–215

    2024

  27. [35]

    Rustan M

    K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. InLogic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, Vol. 6355. Springer, 348–370

    2010

  28. [36]

    Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert: a formally verified optimizing compiler. InERTS 2016: Embedded Real Time Software and Systems, 8th European Congress

    2016

  29. [37]

    Haonan Li, Yu Hao, Yizhuo Zhai, and Zhiyun Qian. 2024. Enhancing static analysis for practical bug detection: An LLM-integrated approach.Proceedings of the ACM on Programming Languages8, OOPSLA1 (2024), 474–499

    2024

  30. [38]

    Minghai Lu, Benjamin Delaware, and Tianyi Zhang. 2024. Proof Automation with Large Language Models. InProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. 1509–1520

    2024

  31. [39]

    2025.Adaptive Proof Refinement with LLM-Guided Strategy Selection

    Minghai Lu, Zhe Zhou, Danning Xie, Songlin Jia, Benjamin Delaware, and Tianyi Zhang. 2025.Adaptive Proof Refinement with LLM-Guided Strategy Selection. arXiv:2510.25103 [cs] doi:10.48550/arXiv.2510.25103

    2025 doi

  32. [40]

    Zhengxiong Luo, Huan Zhao, Dylan Wolff, Cristian Cadar, and Abhik Roychoud- hury. 2026. Agentic Concolic Execution. In2026 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, 37–55

    2026

  33. [41]

    Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. SpecGen: Auto- mated Generation of Formal Program Specifications via Large Language Models . In2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE Computer Society, Los Alamitos, CA, USA, 16–28

    2025

  34. [42]

    Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. 2010. Toward a verified relational database management system. InProceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 237–248

    2010

  35. [43]

    Roy L McCasland, Alan Bundy, and Patrick F Smith. 2017. MATHsAiD: Automated mathematical theory exploration.Applied Intelligence47, 3 (2017), 585–606

    2017

  36. [44]

    Md Rakib Hossain Misu, Cristina V Lopes, Iris Ma, and James Noble. 2024. To- wards AI-assisted synthesis of verified Dafny methods.Proceedings of the ACM on Software Engineering1, FSE (2024), 812–835

    2024

  37. [45]

    Omar Montano-Rivas, Roy McCasland, Lucas Dixon, and Alan Bundy. 2012. Scheme-based theorem discovery and concept invention.Expert Systems with Applications39, 2 (2012), 1637–1646

    2012

  38. [46]

    Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. InVerification, Model Checking, and Abstract Interpretation - 17th International Conference, Vol. 9583. Springer, 41–62

    2016

  39. [47]

    Daye Nam, Andrew Macvean, Vincent Hellendoorn, Bogdan Vasilescu, and Brad Myers. 2024. Using an LLM to help with code understanding. InProceedings of the IEEE/ACM 46th International Conference on Software Engineering. 1–13

    2024

  40. [48]

    Huu Hai Nguyen and Wei-Ngan Chin. 2008. Enhancing program verification with lemmas. InInternational Conference on Computer Aided Verification. Springer, 355–369

    2008

  41. [49]

    2002.Isabelle/HOL: a proof assistant for higher-order logic

    Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. 2002.Isabelle/HOL: a proof assistant for higher-order logic. Springer

    2002

  42. [50]

    2025.Function Calling Developer Documentation

    OpenAI. 2025.Function Calling Developer Documentation. https://developers. openai.com/api/docs/guides/function-calling

    2025

  43. [51]

    Baptiste Pollien, Christophe Garion, Gautier Hattenberger, Pierre Roux, and Xavier Thirioux. 2021. Verifying the mathematical library of an UAV autopilot with frama-C. InInternational Conference on Formal Methods for Industrial Critical Systems. Springer, 167–173

    2021

  44. [52]

    Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. 2020. Gen- erating correctness proofs with neural networks. InProceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Lan- guages. 1–10

    2020

  45. [53]

    Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer. 2023. Passport: Improving automated formal verification using identifiers.ACM Transactions on Programming Languages and Systems45, 2 (2023), 1–30

    2023

  46. [54]

    Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman, Dylan Zhang, Talia Ringer, and Yuriy Brun. 2024. QEDCartographer: Automating formal verification using reward-free Reinforcement Learning. In2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE ...

    2024

  47. [55]

    2023.Formal verification: an essential toolkit for modern VLSI design

    Erik Seligman, Tom Schubert, and MV Achutha Kiran Kumar. 2023.Formal verification: an essential toolkit for modern VLSI design. Elsevier

    2023

  48. [56]

    Aishwarya Sivaraman, Alex Sanchez-Stern, Bretton Chen, Sorin Lerner, and Todd Millstein. 2022. Data-driven lemma synthesis for interactive proofs.Proceedings of the ACM on Programming Languages6, OOPSLA2 (2022), 505–531

    2022

  49. [57]

    Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. 2017. Automated lemma synthesis in symbolic-heap separation logic.Proceedings of the ACM on Programming Languages2, POPL (2017), 1–29

    2017

  50. [58]

    Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. 2024. An in-context learning agent for formal theorem-proving. In First Conference on Language Modeling. 1–27

    2024

  51. [59]

    Ferreira, Sorin Lerner, and Emily First

    Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, Joao F. Ferreira, Sorin Lerner, and Emily First. 2025. Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification . In2025 IEEE/ACM 47th International Conference on ...

    2025

  52. [60]

    Haoxin Tu, Seongmin Lee, Yuxian Li, Peng Chen, Lingxiao Jiang, and Marcel Böhme. 2026. Cottontail: Large Language Model-Driven Concolic Execution for Highly Structured Test Input Generation. In2026 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, 2064–2082

    2026

  53. [61]

    Haoxin Tu, Huan Zhao, Yahui Song, Mehtab Zafar, Ruijie Meng, and Abhik Roy- choudhury. 2025. Agentic Program Verification.arXiv preprint arXiv:2511.17330 (2025)

    2025 arXiv

  54. [62]

    Zhongyi Wang, Tengjie Lin, Mingshuai Chen, Haokun Li, Mingqi Yang, Xiao Yi, Shengchao Qin, Yixing Luo, Xiaofeng Li, Bin Gu, Liqiang Lu, and Jianwei Yin

  55. [63]

    Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, and Cong Tian. 2024. Enchanting program specification synthesis by Large Language Models using static analysis and program veri- fication. InInternational Conference on Computer Aid...

    2024

  56. [64]

    Guangyuan Wu, Weining Cao, Yuan Yao, Hengfeng Wei, Taolue Chen, and Xiaoxing Ma. 2024. LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference. InProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE). 406–417

    2024

  57. [65]

    Yin Wu, Xiaofei Xie, Chenyang Peng, Dijun Liu, Hao Wu, Ming Fan, Ting Liu, and Haijun Wang. 2024. AdvScanner: Generating adversarial smart contracts to exploit reentrancy vulnerabilities using LLM and static analysis. InProceedings of the 39th IEEE/ACM International Conference...

    2024

  58. [66]

    Chunqiu Steven Xia, Matteo Paltenghi, Jia Le Tian, Michael Pradel, and Lingming Zhang. 2024. Fuzz4all: Universal fuzzing with Large Language Models. InPro- ceedings of the IEEE/ACM 46th International Conference on Software Engineering. 1–13

    2024

  59. [67]

    Qiyuan Xu, Xiaokun Luan, Renxi Wang, Joshua Ong Jun Leang, Peixin Wang, Haonan Li, Wenda Li, and Conrad Watt. 2026. Neural Theorem Proving for Verification Conditions: A Real-World Benchmark. InThe Fourteenth International Conference on Learning Representations

    2026

  60. [68]

    Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu

    Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu. 2025. AutoVerus: Automated Proof Genera- tion for Rust Code.Proc. ACM Program. Lang.9, OOPSLA2...

    2025

  61. [69]

    Kaiyu Yang and Jia Deng. 2019. Learning to prove theorems via interacting with proof assistants. InInternational Conference on Machine Learning. PMLR, 6984–6994

    2019

  62. [70]

    Weikun Yang, Grigory Fedyukovich, and Aarti Gupta. 2019. Lemma synthesis for automating induction over algebraic data types. InInternational Conference on Principles and Practice of Constraint Programming. Springer, 600–617

    2019

  63. [71]

    Xinyue Zuo, Yifan Zhang, Hongshu Wang, Yufan Cai, Zhe Hou, Jing Sun, and Jin Song Dong. 2025. PAT-Agent: Autoformalization for Model Checking. In Proceedings of the 40th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2122–2133. 12

    2025

  64. [2010]

    Deductive verification of cryptographic software.Innovations in Systems and Software Engineering6, 3 (2010), 203–218

    2010

  65. [2014]

    InNASA Formal Methods Symposium

    Formal Verification of kLIBC with the WP Frama-C Plug-in. InNASA Formal Methods Symposium. Springer, 343–358

  66. [2024]

    Can Large Language Models transform natural language intent into formal method postconditions?Proceedings of the ACM on Software Engineering1, FSE (2024), 1889–1912

    2024

  67. [2026]

    ACM Program

    A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs.Proc. ACM Program. Lang.OOPSLA1 (2026)

    2026

Pith tools

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