arxivcs.FLcs.AIcs.SE2026-07-07
Harnessing Code Agents for Automatic Software Verification
Shuangxiang Kan, Shuanglong Kan, Sebastian Ertel
Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs automatically, yet exist…