arXiv cs.AI
· Papers
Harnessing Code Agents for Automatic Software Verification
arXiv:2607.06341v1 Announce Type: cross Abstract: 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,