LLMs propose, verifiers check: our work on LLMs and formal verification

Created on October 30, 2026

2026   ·   formal-verification   llms   esbmc   ·   research

A language model can produce a loop invariant, a function contract or a patch in seconds. It cannot tell you whether any of those things is actually correct. A model checker can. Unwinding assertions confirm that a loop bound covers every iteration, k-induction proves properties of unbounded executions, and ranking functions prove that loops terminate. The checker still needs a property to verify, and for deep/nested loops and large codebases the proof often depends on an invariant or contract that no one has written. Each side fills a gap in the other.

Since 2023 our Systems and Software Security (S3) group at the University of Manchester and our collaborators have looked at what happens when the two share a loop. Much of this work has used ESBMC, the SMT-based model checker that we develop. ESBMC combines abstract interpretation through interval analysis, model checking through bounded model checking and k-induction, deductive verification through function contracts [1], and SMT solving. A recent survey looks at how it has become the verification backend for LLM-based tools [2].

flowchart LR
    T["Task<br/>program, property,<br/>or requirement"] --> L["LLM proposes<br/>code, patch, invariant,<br/>contract, spec, translation"]
    L --> V{"Formal tool checks<br/>ESBMC,<br/>automated theorem prover"}
    V -- "holds" --> A["Accepted artifact<br/>with a proof or<br/>bounded guarantee"]
    V -- "fails" --> C["Counterexample<br/>trace, line, property"]
    C --> L

Figure 1. The loop shared by most of the papers below. The LLM never makes the correctness decision; the formal tool does.

Our work since 2023

1. How safe is LLM-generated code?

We started off by asking how often LLM-written code is unsafe, and used ESBMC to find out. More than half of the C programs that GPT-3.5-turbo wrote for our FormAI dataset had at least one vulnerability [3], and a follow-up across nine LLMs found at least 62% [4].

Model checking every completion is too slow for an IDE, so we used these verifier-checked labels to train SecureFalcon, a small classifier that flags vulnerable code instantly on a CPU [5].

Formal tools have blind spots too. On the CASTLE benchmark, ESBMC raised the fewest false alarms but missed vulnerabilities outside the properties it checks, such as weak cryptography, while LLMs got worse as programs grew [6]. A survey chapter covers the wider area [7].

2. Counterexample-guided repair and generation

When ESBMC finds a violation, it returns a counterexample: a concrete input and the execution trace that leads to the failing check. That makes it a precise bug report, so we pass it back to an LLM. ESBMC-AI (posted May 2023) takes the source code, the counterexample and the stack trace and feeds it to an LLM, and ESBMC then re-verifies the patch. It was evaluated on 50k FormAI programs [8]. ESBMC-AI has since been succeeded by Entoli, an open-source agent with formal-verification-based workflows. The same loop also works for neural-network code: ESBMC checked about 81k mutated neural-network programs, and an LLM repaired the bugs that ESBMC found [9]. VeriExploit runs it in reverse: you start with a Solidity counterexample and an LLM generates an attacker contract which re-triggers the bug. That contract is then validated by a model checker and is able to reproduce 85.60% of the bugs in our benchmark [10]. For legacy C code, UnitTenX turns ESBMC counterexamples into readable unit tests [11].

3. LLMs supply what the verifier is missing

Here the LLM writes out the invariants and contracts that a proof needs, and a sound tool then decides whether to believe them.

  • Invariants. ESBMC ibmc replaces each loop with an LLM-generated invariant which a theorem prover then checks. It was able to verify programs that SeaHorn and VeriAbs were unable to verify and went on to receive an ACM SIGSOFT Distinguished Paper Award [12]. VerIbmc takes the same approach using open-weight models on a single local machine and solves 431 of the 499 problems in its best configuration, GPT-OSS-120B [13].
  • Contracts. ConVer takes a top-level property and synthesizes function contracts from it, refining them in a CEGAR-CEGIS loop and achieving 82-96% success on 45 Frama-C programs, the easiest of its four benchmark suites, and as low as 33% on the harder ones [14]. For regression verification, partial LLM-inferred contracts produced zero false equivalence proofs on EqBench-C [15].
  • Agents. Agentic model checking is based on the principle of ‘agents propose, solvers verify’ where the agent works out the specifications and plans the run, with all soundness-critical decisions remaining with the bounded model checker (CBMC and Kani). On mature, heavily fuzzed software it found 68 source-audited defects across 11 projects [16].

4. From prose and other languages to checkable models

SpecVerify uses Claude 3.5 Sonnet in conjunction with ESBMC to derive properties from requirements. On nine of Lockheed Martin’s cyber-physical systems it achieved the same result as NASA’s CoCoSim but with fewer false positives [17]. The models still occasionally misread the specifications, so human review remained necessary. INVAR takes a document (e.g. the USB 2.0 or CXL 4.0 specification) and extracts a transition system from it, which it then checks with NuSMV and reports any missing evidence as a named gap rather than a vacuous pass [18]. With NASA JPL we use an LLM to translate Python into C for ESBMC. The paper makes the caveat that as the translation doesn’t prove equivalence the outcome is only bug finding and not verification [19]; the agent and benchmark are both public.

5. Reviews of the field

Two reviews place this work in a wider context: one which provides a taxonomy of the generative transformations and their recurring patterns in over 100 LLM-based proposals for software verification and falsification [20], and one which is a systematic review of 38 studies on LLM agents, which identifies specification as the bottleneck rather than checking [21].

How the pieces fit together

timeline
    2023 : FormAI dataset
         : ESBMC-AI preprint
    2024 : LLM invariants, ESBMC ibmc
         : Repair of neural-network code
    2025 : FormAI-v2, nine LLMs
         : SecureFalcon, CASTLE
         : SpecVerify, VeriExploit, UnitTenX
    2026 : ConVer, VerIbmc, partial contracts
         : Python translation, INVAR
    2027 : Agentic model checking

Figure 2. Timeline by publication year, or by first preprint for ESBMC-AI and for work not yet at a venue.

The papers all follow the same pattern of division of labor. The LLM does the semantic guessing (what a loop maintains, what a function assumes, what a requirement means). A sound tool provides the guarantee. Over time the LLM has been trusted to do more and more. It started off just being measured, then it was used to repair code under a whole-program verifier, then it was used to write parts of the proof and in the agentic model checking work it’s used to plan the entire run. Invariants and contracts are proved before they are used, so a wrong guess is rejected. Assumptions about the environment are different: they are trusted, not checked. If an LLM writes an assumption that rules out every input reaching an assertion, the verifier reports success vacuously. That is why our pipelines check the evidence itself: each LLM-written harness has a seeded-bug twin that must fail, and INVAR reports missing evidence as a gap rather than a pass. A number of the papers are also direct extensions of one another. FormAI provided the evaluation set for ESBMC-AI and the training data for SecureFalcon. VerIbmc builds on the ibmc invariant work.

The negative results are just as important as the positive ones. CASTLE shows us the limitations of the formal tools. SpecVerify shows that the prose still requires a human to read it. The Python work is very clear that, without a verified translation, the method can find bugs but cannot prove the code correct.

Lessons learned

Benchmarks come with an answer key; production code does not. In recent work an LLM agent drafted verification harnesses for codebases such as the AWS SDK for C++, NVIDIA OpenSMA firmware and vLLM, ESBMC checked them, and maintainers merged 18 fixes upstream, including fixes for two CVEs in the AWS SDK for C++. Five lessons from that work and the papers above, presented at FATTW 2026:

  1. Zero false positives beats a higher proof rate. Developers stop trusting a tool that raises false alarms.
  2. Maintainers fix what arrives with a concrete input. The counterexample is the bug report.
  3. The generator’s quality still propagates. With GPT-4o instead of Claude 3.5 Sonnet, SpecVerify produced 8 false positives instead of 0.
  4. We do not win every benchmark. SeaHorn proves more programs than ibmc, and CoCoSim matches SpecVerify; portfolios beat single tools.
  5. Verifiers have traps too. Zero verification conditions, disabled unwinding assertions and contracts that silently check nothing all look like success, so the evidence itself needs checking.

What comes next

There are three challenges that neither academia nor industry can solve alone:

  • Verification at generation speed. Agents generate code in seconds, while industrial proofs take minutes to hours. Faster tools will not close this gap entirely: program verification is undecidable in general (Rice’s theorem), so some checks can end in a timeout or an unknown verdict. Checking must reuse earlier proofs incrementally and report honestly when it cannot decide.
  • Guarantees for agent workflows. Verifying each agent is not enough to verify the workflow they form; we need compositional contracts between agents.
  • Evidence we can trust. DO-178C, the standard for airborne software, already accepts formal evidence through its formal methods supplement, DO-333, which raises the question of who checks the checker. Witnesses and validators are part of the answer.

Underneath all three sits the problem that every line of work above runs into: how do we validate a specification an LLM has derived from natural language before anything is proved against it?

Join us

We’re looking for PhD students, postdocs and collaborators who are interested in working on these problems (formal methods, program analysis, machine learning etc). Our tools are open source and most of the papers listed above come with the associated artifacts so you can run them. If this is of interest to you then just get in touch with Lucas Cordeiro with a brief note on what you’d like to work on. To talk with the group first, join our public Zulip chat.

References

  • [1] W. Wang, M. Farrell, L. Zhao, and L. C. Cordeiro, “Function Contracts for Bounded Model Checking of C Programs,” CoRR, vol. abs/2610.26089, 2026, doi: 10.48550/arXiv.2610.26089. DOI
  • [2] P. V. Dantas, L. C. Cordeiro, and W. S. S. Júnior, “ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification,” CoRR, vol. abs/2605.26169, 2026, doi: 10.48550/arXiv.2605.26169. DOI
  • [3] N. Tihanyi, T. Bisztray, R. Jain, M. A. Ferrag, L. C. Cordeiro, and V. Mavroeidis, “The FormAI Dataset: Generative AI in Software Security through the Lens of Formal Verification,” in Proceedings of the 19th International Conference on Predictive Models and Data Analytics in Software Engineering, PROMISE 2023, San Francisco, CA, USA, 8 December 2023, S. McIntosh, E. Choi, and S. Herbold, Eds., ACM, 2023, pp. 33–43. doi: 10.1145/3617555.3617874. DOI PDF
  • [4] N. Tihanyi, T. Bisztray, M. A. Ferrag, R. Jain, and L. C. Cordeiro, “How secure is AI-generated code: a large-scale comparison of large language models,” Empir. Softw. Eng., vol. 30, no. 2, p. 47, 2025, doi: 10.1007/s10664-024-10590-1. DOI
  • [5] M. A. Ferrag et al., “SecureFalcon: Are We There Yet in Automated Software Vulnerability Detection With LLMs?,” IEEE Trans. Software Eng., vol. 51, no. 4, pp. 1248–1265, 2025, doi: 10.1109/TSE.2025.3548168. DOI
  • [6] R. A. Dubniczky, K. Z. Horvát, T. Bisztray, M. A. Ferrag, L. C. Cordeiro, and N. Tihanyi, “CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs Towards CWE Detection,” in Theoretical Aspects of Software Engineering - 19th International Symposium, TASE 2025, Limassol, Cyprus, July 14-16, 2025, Proceedings, P. Rümmer and Z. Wu, Eds., in Lecture Notes in Computer Science, vol. 15841. Springer, 2025, pp. 253–272. doi: 10.1007/978-3-031-98208-8_15. DOI PDF
  • [7] N. Tihanyi et al., “Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview,” in Adversarial Example Detection and Mitigation Using Machine Learning, E. Nowroozi, R. Taheri, and L. C. Cordeiro, Eds., Springer, 2026, pp. 33–47. doi: 10.1007/978-3-031-99447-0_3. DOI
  • [8] N. Tihanyi, Y. Charalambous, R. Jain, M. A. Ferrag, and L. C. Cordeiro, “A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification,” in IEEE/ACM International Conference on Automation of Software Test, AST@ICSE 2025, Ottawa, ON, Canada, April 28-29, 2025, A. Zaidman, F. Lonetti, I. Schieferdecker, and R. Subramanyan, Eds., IEEE, 2025, pp. 136–147. doi: 10.1109/AST66626.2025.00020. DOI PDF
  • [9] Y. Charalambous, E. Manino, and L. C. Cordeiro, “Automated Repair of AI Code with Large Language Models and Formal Verification,” CoRR, vol. abs/2405.08848, 2024, doi: 10.48550/arXiv.2405.08848. DOI
  • [10] C. Wei, S. Cai, Y. Charalambous, T. Wu, S. Godboley, and L. C. Cordeiro, “VeriExploit: Automatic Bug Reproduction in Smart Contracts via LLMs and Formal Methods,” in 40th IEEE/ACM International Conference on Automated Software Engineering, ASE 2025, Seoul, Korea, Republic of, November 16-20, 2025, IEEE, 2025, pp. 1415–1426. doi: 10.1109/ASE63991.2025.00120. DOI PDF
  • [11] Y. Charalambous, C. N. Coelho Jr., L. C. Lamb, and L. C. Cordeiro, “UnitTenX: Generating Tests for Legacy Packages with AI Agents Powered by Formal Verification,” in Proceedings of the Generative Code Intelligence Workshop (GeCoIn 2025) co-located with 28th European Conference on Artificial Intelligence (ECAI 2025), Bologna, Italy, October 26, 2025, E. Iotti, G. Dolcetti, V. Arceri, and S. Maffeis, Eds., in CEUR Workshop Proceedings, vol. 4075. CEUR-WS.org, 2025. Available at: https://ceur-ws.org/Vol-4075/paper5.pdf Link
  • [12] M. A. A. Pirzada, G. Reger, A. Bhayat, and L. C. Cordeiro, “LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling,” in Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE 2024, Sacramento, CA, USA, October 27 - November 1, 2024, V. Filkov, B. Ray, and M. Zhou, Eds., ACM, 2024, pp. 1395–1407. doi: 10.1145/3691620.3695512. DOI
  • [13] M. A. A. Pirzada, J. Parsert, W. Wang, K. Korovin, and L. C. Cordeiro, “Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale,” CoRR, vol. abs/2606.16886, 2026, doi: 10.48550/arXiv.2606.16886. DOI
  • [14] M. A. A. Pirzada, W. Wang, Y. Charalambous, K. Korovin, and L. C. Cordeiro, “ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification,” CoRR, vol. abs/2605.27051, 2026, doi: 10.48550/arXiv.2605.27051. DOI
  • [15] Y. Charalambous, R. Menezes, Y. Sun, and L. C. Cordeiro, “Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification,” CoRR, vol. abs/2607.10291, 2026, doi: 10.48550/arXiv.2607.10291. DOI
  • [16] Y. Sun, J. Liu, H. Alqasimi, L. C. Cordeiro, D. Kroening, and J. Xue, “Agentic Model Checking,” in 49th IEEE/ACM International Conference on Software Engineering, ICSE 2027, IEEE/ACM, 2027. Link PDF
  • [17] W. Wang, M. Farrell, L. C. Cordeiro, and L. Zhao, “Supporting Software Formal Verification with Large Language Models: An Experimental Study,” in 33rd IEEE International Requirements Engineering Conference, RE 2025, Valencia, Spain, September 1-5, 2025, IEEE, 2025, pp. 423–431. doi: 10.1109/RE63999.2025.00049. DOI
  • [18] S. Sood, J. Goodacre, and L. C. Cordeiro, “Large-Language-Model-Aided Intent Verification via Grounded Obligation Models,” in 19th IEEE International Symposium on Embedded Multicore/Many-core Systems-on-Chip, MCSoC 2026, IEEE, 2026. PDF
  • [19] S. Shivaji, K. Havelund, N. Lobakhina, L. C. Cordeiro, and A. Pinto, “LLM-Assisted Translation and Bounded Model Checking of Python Code,” in International Symposium on AI Verification (AISoLA), 2026. PDF
  • [20] V. A. Braberman, F. Bonomo-Braberman, Y. Charalambous, J. G. Colonna, L. C. Cordeiro, and R. de Freitas, “Generative Transformations and Patterns in LLM-Native Approaches for Software Verification and Falsification,” CoRR, vol. abs/2404.09384, 2024, doi: 10.48550/arXiv.2404.09384. DOI
  • [21] P. V. Dantas, L. C. Cordeiro, E. Nowroozi, and N. Tihanyi, “Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement,” CoRR, vol. abs/2608.14590, 2026, doi: 10.48550/arXiv.2608.14590. DOI