Formal Verification of LLM-Generated Code

gist

In his FATTW 2026 slides, Manchester's Lucas Cordeiro argues that AI now writes code faster than anyone can check it, and the fix is letting language models guess proof ingredients while the ESBMC model checker confirms them. A model-checked study of 310,531 C programs found at most 15.48% of any model's code could be verified, while LLM-assisted pipelines proved programs soundly and found real CVEs.

ideas

• The verification gap. Across nine LLMs only 8.27% of generated C programs passed formal verification, and agents remove the human reviewer, so neither more tests nor an LLM judge can certify the code.
• Suggest, then confirm. Models propose test seeds, loop invariants, contracts or specifications; a sound engine checks them, so a bad guess costs time rather than correctness, except for specifications.
• Three patterns with results. FuSeBMC won Test-Comp 2026 categories; ibmc's LLM invariants proved up to 101 of 133 benchmarks with no wrong verdicts; SpecVerify matched 79.31% of expert properties with zero false positives using Claude 3.5 Sonnet but eight with GPT-4o.
• Real code, real fixes. With LLM-drafted harnesses, ESBMC found two CVEs in the AWS SDK for C++ Base64 decoder, an NVIDIA firmware abort and vLLM flag crashes, with 18 fixes merged upstream.
• Still open. Verification must keep pace with generation, cover multi-agent workflows, and produce evidence that can itself be checked.

quotes