mlsanityData to 14 Oct 2026

Clover: Closed-Loop Verifiable Code Generation

arXiv 2310.17807 ↗First posted 26 Oct 2023cs.AI cs.LG cs.SEcited by 67

Not on the map. Why?

Abstract (arXiv)

The use of large language models for code generation is a rapidly growing trend in software development. However, without effective methods for ensuring the correctness of generated code, this trend could lead to undesirable outcomes. In this paper, we introduce a new approach for addressing this challenge: the Clover paradigm, short for Closed-Loop Verifiable Code Generation, which uses consistency checking to provide a strong filter for incorrect code. Clover performs consistency checks among code, docstrings, and formal annotations. The checker is implemented using a novel integration of formal verification tools and large language models. We provide a theoretical analysis to support our thesis that Clover should be effective at consistency checking. We also empirically investigate its performance on a hand-designed dataset (CloverBench) featuring annotated Dafny programs at a textbook level of difficulty. Experimental results show that for this dataset: (i) LLMs are reasonably successful at automatically generating formal specifications; and (ii) our consistency checker achieves a promising acceptance rate (up to 87%) for correct instances while maintaining zero tolerance for adversarial incorrect ones (no false positives). Clover also discovered 6 incorrect programs in the existing human-written dataset MBPP-DFY-50.

Key facts. Cited by 67 papers in the map (data through 14 Oct 2026). Builds on 37 of its 74 references that are in the map. First posted on arXiv 26 Oct 2023.

Builds on

37 of 74 references.

References · 37

  1. 2023GPT-4 Technical Reportcited by 18,396
  2. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,459
  3. 2021Training Verifiers to Solve Math Word Problemscited by 10,109
  4. 2021Evaluating Large Language Models Trained on Codecited by 8,320
  5. 2022Self-Consistency Improves Chain of Thought Reasoning in Language Modelscited by 5,708
  6. 2022PaLM: Scaling Language Modeling with Pathwayscited by 5,326
  7. 2021Program Synthesis with Large Language Modelscited by 3,637
  8. 2023Self-Refine: Iterative Refinement with Self-Feedbackcited by 3,442
  9. 2023Sparks of Artificial General Intelligence: Early experiments with GPT-4cited by 2,592
  10. 2022Competition-Level Code Generation with AlphaCodecited by 1,462
  11. 2023Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generationcited by 1,391
  12. 2023Teaching Large Language Models to Self-Debugcited by 988
25 more
  1. 2021Measuring Coding Challenge Competence With APPScited by 902
  2. 2022DS-1000: A Natural and Reliable Benchmark for Data Science Code Generationcited by 452
  3. 2021Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributionscited by 431
  4. 2022CodeT: Code Generation with Generated Testscited by 384
  5. 2022Self-critiquing models for assisting human evaluatorscited by 380
  6. 2023Automatically Correcting Large Language Models: Surveying the landscape of diverse self-correction strategiescited by 238
  7. 2022Binding Language Models in Symbolic Languagescited by 228
  8. 2023Is Self-Repair a Silver Bullet for Code Generation?cited by 197
  9. 2022Do Users Write More Insecure Code with AI Assistants?cited by 192
  10. 2022Natural Language to Code Translation with Executioncited by 124
  11. 2022Lost at C: A User Study on the Security Implications of Large Language Model Code Assistantscited by 91
  12. 2022Natural Language to Code Generation in Interactive Data Science Notebookscited by 87
  13. 2022Coder Reviewer Reranking for Code Generationcited by 84
  14. 2022Top-Down Synthesis for Library Learningcited by 58
  15. 2023Verus: Verifying Rust Programs using Linear Ghost Types (extended version)cited by 53
  16. 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
  17. 2021In-IDE Code Generation from Natural Language: Promise and Challengescited by 42
  18. 2023A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verificationcited by 42
  19. 2022Formal Specifications from Natural Languagecited by 33
  20. 2022Fault-Aware Neural Code Rankerscited by 33
  21. 2023Vulnerabilities in AI Code Generators: Exploring Targeted Data Poisoning Attackscited by 33
  22. 2023What do LLMs need to Synthesize Correct Router Configurations?cited by 29
  23. 2023TRACED: Execution-aware Pre-training for Source Codecited by 27
  24. 2015Program Synthesis from Polymorphic Refinement Typescited by 20
  25. 2022CrossBeam: Learning to Search in Bottom-Up Program Synthesiscited by 18

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2024: 14; 2025: 20; 2026: 33.

67 papers.

Sort:

By area:

  1. 2025ACECODER: Acing Coder RL via Automated Test-Case Synthesiscited by 93
  2. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  3. 2024Agents in Software Engineering: Survey, Landscape, and Visioncited by 60
  4. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  5. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 57
  6. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 49
  7. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 35
  8. 2025VERINA: Benchmarking Verifiable Code Generationcited by 34
  9. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 33
  10. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 20
  11. 2025Proving the Coding Interview: A Benchmark for Formally Verified Code Generationcited by 19
  12. 2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofscited by 18
38 more
  1. 2025Vidarc: Embodied Video Diffusion Model for Closed-loop Controlcited by 15
  2. 2025VeruSAGE: A Study of Agent-Based Verification for Rust Systemscited by 12
  3. 2024Laurel: Unblocking Automated Verification with Large Language Modelscited by 11
  4. 2024Guiding Enumerative Program Synthesis with Large Language Modelscited by 9
  5. 2025VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Veruscited by 9
  6. 2025ProofWright: Towards Agentic Formal Verification of CUDAcited by 9
  7. 2026Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agentscited by 9
  8. 2025OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verificationcited by 8
  9. 2026SEVerA: Verified Synthesis of Self-Evolving Agentscited by 8
  10. 2026Faithful Autoformalization via Roundtrip Verification and Repaircited by 8
  11. 2024Joint Verification and Refinement of Language Models for Safety-Constrained Planningcited by 6
  12. 2025Dafny as Verification-Aware Intermediate Language for Code Generationcited by 6
  13. 2025Inferring multiple helper Dafny assertions with LLMscited by 4
  14. 2026Neural Theorem Proving for Verification Conditions: A Real-World Benchmarkcited by 4
  15. 2026Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systemscited by 4
  16. 2024forallutoexistsval: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Taskscited by 3
  17. 2025Next Steps in LLM-Supported Java Verificationcited by 3
  18. 2025Can LLMs Enable Verification in Mainstream Programming?cited by 3
  19. 2026NERFIFY: A Multi-Agent Framework for Turning NeRF Papers into Codecited by 3
  20. 2026Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalizationcited by 3
  21. 2024Generative transformations and patterns in LLM-native approaches for software verification and falsificationcited by 2
  22. 2025Do AI models help produce verified bug fixes?cited by 2
  23. 2025MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verificationcited by 2
  24. 2026Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Inductioncited by 2
  25. 2026Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiabilitycited by 2
  26. 2026Intent-aligned Formal Specification Synthesis via Traceable Refinementcited by 2
  27. 2026Certified Program Synthesis with a Multi-Modal Verifiercited by 2
  28. 2026Vero: Can AI Agents Build Formally Verified Software Repositories?cited by 2
  29. 2024Assured Automatic Programming via Large Language Modelscited by 1
  30. 2025Towards a Probabilistic Framework for Analyzing and Improving LLM-Enabled Softwarecited by 1
  31. 2026Fidelity Probes for Specification--Code Alignmentcited by 1
  32. 2026Automating Formal Verification with Reinforcement Learning and Recursive Inferencecited by 1
  33. 2026Formal Disco: Scalable Open-Ended Generation of Formally Verified Programscited by 1
  34. 2025From Scientific Texts to Verifiable Code: Automating the Process with Transformerscited by 0
  35. 2025Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMscited by 0
  36. 2025LLM-Based Config Synthesis requires Disambiguationcited by 0
  37. 2025On Integrating Large Language Models and Scenario-Based Programming for Improving Software Reliabilitycited by 0
  38. 2026TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamplescited by 0

50 most cited of 67 All 67 (JSON)