# ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 34 references that are in the map.
- First posted on arXiv 26 May 2026.

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

- [Practical Program Repair in the Era of Large Pre-trained Language Models](https://mlsanity.com/paper/2210.14179/) (2022)
- [Evaluating Language Models for Efficient Code Generation](https://mlsanity.com/paper/2408.06450/) (2024)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [Large Language Model (LLM) for Software Security: Code Analysis, Malware Analysis, Reverse Engineering](https://mlsanity.com/paper/2504.07137/) (2025)
- [Towards Effectively Leveraging Execution Traces for Program Repair with Code LLMs](https://mlsanity.com/paper/2505.04441/) (2025)
- [ESBMC v7.4: Harnessing the Power of Intervals](https://mlsanity.com/paper/2312.14746/) (2023)
- [A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs](https://mlsanity.com/paper/2512.24594/) (2025)
- [PolyVer: A Compositional Approach for Polyglot System Modeling and Verification](https://mlsanity.com/paper/2503.03207/) (2025)
- [Array-Carrying Symbolic Execution for Function Contract Generation](https://mlsanity.com/paper/2602.23216/) (2026)

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

- [Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification](https://mlsanity.com/paper/2607.10291/) (2026)

## Abstract (arXiv)

Formal verification of large C programs is impeded by state-space explosion: Bounded Model Checking (BMC) tools must encode the entire state space up to the predetermined bound by unrolling all nested constructs. We present ConVer, a top-down compositional verification tool. Given a C program with a top-level assertion, ConVer decomposes verification top-down: it uses a large language model (LLM) to synthesise function contracts from the system property, then alternates system-level and function-level checks in a CEGAR-CEGIS loop, refining contracts whenever a check fails via SMART ICE learning. We evaluate ConVer on four benchmark suites of increasing difficulty and against other state-of-the-art (SOTA) tools. On the Frama-C benchmark of 45 simple C programs, ConVer achieves 82-96% verification success across three LLM backends, with 93-95% of converged programs requiring only a single CEGAR-CEGIS iteration. On the X.509 parser benchmark (6~programs) and LF2C-Simple suite (17 programs), ConVer achieves 33-50% and 82-88% success respectively. On the VerifyThis suite of 11 recursive and loop-intensive programs, the Pre-Abstraction strategy achieves 55-64% success. In addition, we present ESBMC-LF a preprocessor tool that converts LF models to C while preserving the properties of the LF files, enabling ConVer to verify them. We transpile the LF Verifier Benchmarks using ESBMC-LF to C; we denote those LF-Hard. We show that ConVer successfully verifies 67% of LF-Hard benchmarks overall.