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, uses those proofs to break the problem into simpler parts, automatically identifies which of those parts were successfully proven, and iterates on the remaining parts to build a correct proof that is guaranteed to be sound, despite the reliance on unsound LLMs. We evaluate Cobblestone on four benchmarks of open-source Coq projects, controlling for training data leakage. Fully automatically, Cobblestone outperforms state-of-the-art non-LLM tools, and proves many theorems that other LLM-based tools cannot, and on many benchmarks, outperforms them. Each Cobblestone run costs only $1.25 and takes 14.7 minutes, on average. Cobblestone can also be used with external input, from a user or another tool, providing a proof structure or relevant lemmas. Evaluated with such an oracle, Cobblestone proves up to 58% of theorems. Overall, our research shows that tools can make use of partial progress and external input to more effectively automate formal verification.
@inproceedings{Kasibatla26icse,
author = {Saketh Ram Kasibatla and Arpan Agrawal and Yuriy Brun and
Sorin Lerner and Talia Ringer and Emily First},
title =
{Cobblestone:
A Divide-and-Conquer Approach for Automating Formal Verification},
booktitle = {Proceedings of the 48th International Conference on Software Engineering (ICSE)},
venue = {ICSE},
address = {Rio de Janeiro, Brazil},
month = {April},
date = {15--17},
year = {2026},
pages = {714--726},
doi = {10.1145/3744916.3773178},
accept = {$\frac{160}{660} \approx 24\%$ (1st cycle)},
note = {ACM artifact badges granted:
Artifact Available,
Artifact Reusable.
DOI:
10.1145/3744916.3773178,
arXiv: abs/2410.19940},
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, uses those
proofs to break the problem into simpler parts, automatically identifies
which of those parts were successfully proven, and iterates on the remaining
parts to build a correct proof that is guaranteed to be sound, despite the
reliance on unsound LLMs. We evaluate Cobblestone on four benchmarks of
open-source Coq projects, controlling for training data leakage. Fully
automatically, Cobblestone outperforms state-of-the-art non-LLM tools, and
proves many theorems that other LLM-based tools cannot, and on many
benchmarks, outperforms them. Each Cobblestone run costs only $1.25 and takes
14.7 minutes, on average. Cobblestone can also be used with external input,
from a user or another tool, providing a proof structure or relevant lemmas.
Evaluated with such an oracle, Cobblestone proves up to 58% of theorems.
Overall, our research shows that tools can make use of partial progress and
external input to more effectively automate formal verification.},
fundedBy = {NSF CCF-2210243,
Defense Advanced Research Projects Agencies (DARPA) under Contract No. HR0011-24-2-0307},
}