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

arXiv: https://arxiv.org/abs/2410.19940 · HTML: https://mlsanity.com/paper/2410.19940/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 34 of its 88 references that are in the map.
- First posted on arXiv 25 Oct 2024.

## Builds on (most cited first, 30 of 34)

- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [PaLM: Scaling Language Modeling with Pathways](https://mlsanity.com/paper/2204.02311/) (2022)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [Least-to-Most Prompting Enables Complex Reasoning in Large Language Models](https://mlsanity.com/paper/2205.10625/) (2022)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [Graph of Thoughts: Solving Elaborate Problems with Large Language Models](https://mlsanity.com/paper/2308.09687/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Complexity-Based Prompting for Multi-Step Reasoning](https://mlsanity.com/paper/2210.00720/) (2022)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Navigate through Enigmatic Labyrinth A Survey of Chain of Thought Reasoning: Advances, Frontiers and Future](https://mlsanity.com/paper/2309.15402/) (2023)
- [Fairness Testing: Testing Software for Discrimination](https://mlsanity.com/paper/1709.03221/) (2017)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data](https://mlsanity.com/paper/2402.08957/) (2024)
- [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019)
- [Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving](https://mlsanity.com/paper/2305.16366/) (2023)
- [Learning to Reason in Large Theories without Imitation](https://mlsanity.com/paper/1905.10501/) (2019)
- [Proving Theorems Recursively](https://mlsanity.com/paper/2405.14414/) (2024)

## Built on by (most cited first, 9 of 9)

- [Large Language Model Reasoning Failures](https://mlsanity.com/paper/2602.06176/) (2026)
- [Agentic Code Reasoning](https://mlsanity.com/paper/2603.01896/) (2026)
- [Clarifying Before Reasoning: A Coq Prover with Structural Context](https://mlsanity.com/paper/2507.02541/) (2025)
- [Certified Program Synthesis with a Multi-Modal Verifier](https://mlsanity.com/paper/2604.16584/) (2026)
- [On Reasoning-Centric LLM-based Automated Theorem Proving](https://mlsanity.com/paper/2604.19558/) (2026)
- [Harnessing Code Agents for Automatic Software Verification](https://mlsanity.com/paper/2607.06341/) (2026)
- [PROMISE: Proof Automation as Structural Imitation of Human Reasoning](https://mlsanity.com/paper/2604.05399/) (2026)
- [LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation](https://mlsanity.com/paper/2605.01394/) (2026)
- [ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents](https://mlsanity.com/paper/2610.03796/) (2026)

## Abstract (arXiv)

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.