# Lemur: Integrating Large Language Models in Automated Program Verification

arXiv: https://arxiv.org/abs/2310.04870 · HTML: https://mlsanity.com/paper/2310.04870/

## Key facts

- Cited by 49 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 29 references that are in the map.
- First posted on arXiv 7 Oct 2023.

## Builds on (most cited first, 9 of 9)

- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [Sorting and Transforming Program Repair Ingredients via Deep Learning Code Similarities](https://mlsanity.com/paper/1707.04742/) (2017)

## Built on by (most cited first, 30 of 49)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (2024)
- [Frontier AI's Impact on the Cybersecurity Landscape](https://mlsanity.com/paper/2504.05408/) (2025)
- [A Contemporary Survey of Large Language Model Assisted Program Analysis](https://mlsanity.com/paper/2502.18474/) (2025)
- [Towards Reliable Code-as-Policies: A Neuro-Symbolic Framework for Embodied Task Planning](https://mlsanity.com/paper/2510.21302/) (2025)
- [MCP-Solver: Integrating Language Models with Constraint Programming Systems](https://mlsanity.com/paper/2501.00539/) (2024)
- [Guiding Enumerative Program Synthesis with Large Language Models](https://mlsanity.com/paper/2403.03997/) (2024)
- [VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus](https://mlsanity.com/paper/2510.25015/) (2025)
- [Generating Streamlining Constraints with Large Language Models](https://mlsanity.com/paper/2408.10268/) (2024)
- [Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview](https://mlsanity.com/paper/2503.10784/) (2025)
- [Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification](https://mlsanity.com/paper/2510.03469/) (2025)
- [Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis](https://mlsanity.com/paper/2509.21629/) (2025)
- [Inferring multiple helper Dafny assertions with LLMs](https://mlsanity.com/paper/2511.00125/) (2025)
- [Next Steps in LLM-Supported Java Verification](https://mlsanity.com/paper/2502.01573/) (2025)
- [Integrating Expert Knowledge into Logical Programs via LLMs](https://mlsanity.com/paper/2502.12275/) (2025)
- [PAT-Agent: Autoformalization for Model Checking](https://mlsanity.com/paper/2509.23675/) (2025)
- [ExVerus: Verus Proof Repair via Counterexample Reasoning](https://mlsanity.com/paper/2603.25810/) (2026)
- [Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair](https://mlsanity.com/paper/2605.17475/) (2026)
- [Generative transformations and patterns in LLM-native approaches for software verification and falsification](https://mlsanity.com/paper/2404.09384/) (2024)
- [Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems](https://mlsanity.com/paper/2511.14435/) (2025)
- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capability](https://mlsanity.com/paper/2605.28602/) (2026)
- [Towards Automated Formal Verification of Backend Systems with LLMs](https://mlsanity.com/paper/2506.10998/) (2025)
- [LLM For Loop Invariant Generation and Fixing: How Far Are We?](https://mlsanity.com/paper/2511.06552/) (2025)
- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)
- [Evaluating LLM-Generated ACSL Annotations for Formal Verification](https://mlsanity.com/paper/2602.13851/) (2026)
- [Fidelity Probes for Specification--Code Alignment](https://mlsanity.com/paper/2605.17246/) (2026)
- [Lucy: Think and Reason to Solve Text-to-SQL](https://mlsanity.com/paper/2407.05153/) (2024)

## Abstract (arXiv)

The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of transition rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks.