Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification

arXiv:2410.19940v4 Announce Type: replace-cross Abstract: Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but requires significant effort and expertise. Machine learning can automatically synthesize proofs, but such tools are able to prove only a fraction of desired software properties. We introduce Cobblestone, a divide-and-conquer approach for proof synthesis. Cobblestone uses a large language model (LLM) to generate potential proofs,