ConVer: LLM-Synthesized Contracts Enable Scalable Formal Verification of Large C Programs
arXiv·medium signal
Pirzada et al. present ConVer, a compositional verification tool that overcomes bounded model checking's state-space explosion by using LLMs to synthesize function contracts and loop invariants. Given a C program with an assertion, ConVer decomposes verification top-down, alternating system-level and function-level checks. This hybrid approach lets formal verification scale to real-world codebases where pure BMC times out.