# Can ChatGPT support software verification?

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

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 31 references that are in the map.
- First posted on arXiv 4 Nov 2023.

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

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [Extending Context Window of Large Language Models via Positional Interpolation](https://mlsanity.com/paper/2306.15595/) (2023)
- [InCoder: A Generative Model for Code Infilling and Synthesis](https://mlsanity.com/paper/2204.05999/) (2022)
- [CodeT: Code Generation with Generated Tests](https://mlsanity.com/paper/2207.10397/) (2022)
- [Check Your Facts and Try Again: Improving Large Language Models with External Knowledge and Automated Feedback](https://mlsanity.com/paper/2302.12813/) (2023)
- [Impact of Code Language Models on Automated Program Repair](https://mlsanity.com/paper/2302.05020/) (2023)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)

## Built on by (most cited first, 14 of 14)

- [LLMDFA: Analyzing Dataflow in Code with Large Language Models](https://mlsanity.com/paper/2402.10754/) (2024)
- [A Contemporary Survey of Large Language Model Assisted Program Analysis](https://mlsanity.com/paper/2502.18474/) (2025)
- [Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods](https://mlsanity.com/paper/2406.15540/) (2024)
- [Helping LLMs Improve Code Generation Using Feedback from Testing and Static Analysis](https://mlsanity.com/paper/2412.14841/) (2024)
- [Next Steps in LLM-Supported Java Verification](https://mlsanity.com/paper/2502.01573/) (2025)
- [Generative transformations and patterns in LLM-native approaches for software verification and falsification](https://mlsanity.com/paper/2404.09384/) (2024)
- [Do AI assistants help students write formal specifications? A study with ChatGPT and the B-Method](https://mlsanity.com/paper/2502.07789/) (2025)
- [One For All: LLM-based Heterogeneous Mission Planning in Precision Agriculture](https://mlsanity.com/paper/2506.10106/) (2025)
- [Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability](https://mlsanity.com/paper/2604.00280/) (2026)
- [IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking](https://mlsanity.com/paper/2604.03232/) (2026)
- [A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning](https://mlsanity.com/paper/2512.15816/) (2025)
- [As You Wish: Mission Planning with Formal Verification using LLMs in Precision Agriculture](https://mlsanity.com/paper/2606.18519/) (2026)
- [AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis](https://mlsanity.com/paper/2606.20969/) (2026)
- [An Empirical Study of LLM-Generated Specifications for VeriFast](https://mlsanity.com/paper/2606.26490/) (2026)

## Abstract (arXiv)

Large language models have become increasingly effective in software engineering tasks such as code generation, debugging and repair. Language models like ChatGPT can not only generate code, but also explain its inner workings and in particular its correctness. This raises the question whether we can utilize ChatGPT to support formal software verification. In this paper, we take some first steps towards answering this question. More specifically, we investigate whether ChatGPT can generate loop invariants. Loop invariant generation is a core task in software verification, and the generation of valid and useful invariants would likely help formal verifiers. To provide some first evidence on this hypothesis, we ask ChatGPT to annotate 106 C programs with loop invariants. We check validity and usefulness of the generated invariants by passing them to two verifiers, Frama-C and CPAchecker. Our evaluation shows that ChatGPT is able to produce valid and useful invariants allowing Frama-C to verify tasks that it could not solve before. Based on our initial insights, we propose ways of combining ChatGPT (or large language models in general) and software verifiers, and discuss current limitations and open issues.