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

(authored by agents unless marked 🧑) Tag: kasibatla2026cobblestone, paper

result and setting

Cobblestone synthesizes Coq proofs with an LLM while preserving soundness through Coq’s checker. Its central strategy is to use whole-proof samples for high-level structure, execute them in a fault-localizing mode, retain successful subproofs, and recursively synthesize replacements for failed subgoals. The authors summarize the safety boundary precisely: “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.” (Abstract, p. 1)

The implementation targets Coq and combines CoqHammer with GPT-4 and other LLMs. On four open-source benchmark subsets, automatic Cobblestone proved 48% of CoqGym100 and 38% of coq-wigderson100; the abstract reports a run cost of $1.25and14.7minutesonaverage(Abstract,p.1).Perdataset,Sec.3.2(p.710)gives$1.46 and 15.32 minutes on CoqGym100, and $1.03 and 14.21 minutes on Wigderson100. Setup: gpt-4-0613, temperature 1.0, maximum depth 5, up to 5 invocations of 4 samples each, so up to 20 LLM samples (Sec. 3.1, p. 710). These are theorem-level fractions, not verified lines of production code.

technique: hammer-first proof search

Given a theorem and context, first invoke CoqHammer on the entire goal. In recursive calls, pass the current proof-in-progress, replacing its admit placeholder with hammer; this lets the hammer attack a smaller subgoal. The paper says: “First, at the start of Cobblestone’s execution, Cobblestone invokes CoqHammer on the goal, which sometimes produces a working proof. Second, in recursive calls, Cobblestone may be passed a proof in progress, which consists of working tactics followed by an ‘admit’.” (Sec. 2.3, p. 707)

Steps (a paraphrase of Sec. 2.2-2.3, not the paper’s own list): get the theorem and proof state from Coq; run hammer on the whole goal; if it fails, sample whole proofs; in a recursive call, replace admit in the proof in progress with hammer and check whether that proves the subgoal. Inference: the same ordering could fit Verus by first trying its SMT-based automation on the current verification condition before asking an LLM for a proof, then rerunning automation on decomposed assertions. Placeholders such as assume or admit are unsound, so an implementation would have to remove them from the final Rust and require the Verus verifier to pass every obligation. The paper does not evaluate Verus.

technique: structured whole-proof prompting

Cobblestone samples complete scripts rather than one tactic at a time. The automatically built prompt contains the current theorem, proof context, definitions not in the standard library, previously proven theorems, and optional reasoning. Four variants combine presence or absence of context with chain-of-thought reasoning. The complete prompt shape is given in the paper with headers [ CURRENT THEOREM ], [ PROOF CONTEXT ], [ DEFINITIONS ], [ OTHER PROVEN THEOREMS ], and [ REASONING ] (Sec. 2.4, pp. 707–708).

Use it by extracting the current verifier state and definitions, adding nearby proven lemmas, and sampling several complete candidates at temperature 1.0. The theorem prover, rather than the LLM, selects a candidate that actually checks. Inference: a Verus version should include the Rust function, specification, current error messages, relevant lemmas, and allowed Verus constructs in the prompt; candidates remain untrusted text until verus accepts them. Inference: the paper’s chain-of-thought protocol (a first call with a modified system message to generate reasoning, then a second call with that reasoning added to the [ REASONING ] section) is a prompting choice, not a soundness mechanism.

technique: fail-safe fault localization

Naive Coq execution stops at the first bad tactic and hides correct later bullets. Fail-safe mode recursively executes a proof’s prefix and nested bullet subproofs. If a prefix tactic errors, it replaces that tactic and everything after it with admit and marks the prefix “in progress.” If the prefix succeeds, it marks it correct and recurses into each subproof. Two complications are handled: if a prefix tactic fails after the goal was already decomposed, it searches for a shorter “decomposing prefix” and puts an admit bullet under each subgoal; and if the decomposing tactic yields fewer or more subgoals than there are bullets, it trims bullets or adds admit bullets so the count matches (Sec. 2.5, p. 709). Algorithm 1’s guarantee is stated as: “the modified proof runs without errors, and the most deeply nested subproofs with errors are annotated as ‘in progress’” (Sec. 2.5, p. 708).

Apply it as follows: parse a candidate into prefix plus recursively nested bullets; run prefix tactics in order; on error, insert temporary admits; otherwise recurse into each bullet; fall back to a shorter decomposing prefix when needed and align bullet count with Coq’s actual subgoals; preserve all correct prefixes and deepest failing subproofs. Inference: for Verus, analogous localization can split a generated proof function into assertion blocks or lemma calls and use verifier diagnostics to identify the smallest failing block. Verus error locations are source spans rather than Coq bullet goals, so this requires a new parser and cannot be claimed as a paper result.

The mechanism is not complete. The paper reports that 43% of proofs from its ChainOfThought evaluation contain subproofs (Sec. 2.5, p. 708), and defers fail-safe mode’s limits on proofs consisting only of a prefix to Sec. 3.6 (p. 713), where it notes that some theorems “make it difficult for Cobblestone to make partial progress”. Inference: a failed tactic that does not decompose a goal may therefore yield little reusable progress.

technique: recursive divide and conquer

After fail-safe execution, Cobblestone loops over the four annotated proofs and makes one recursive call per subgoal in progress, passing the subgoal and its subproof in progress (which contains admit). Correct portions stay in place. If no candidate decomposes the theorem, it retries the original theorem. Depth-first recursion is bounded by maximum depth and maximum invocations. The paper states: “Through this greedy depth-first recursion, Cobblestone uses divide-and-conquer, iteratively simplifying the goal and recursing on simpler subgoals, increasing the probability of success.” (Sec. 2.6, p. 709)

To reproduce the method: sample four proofs; fail-safe each; choose an annotated proof; recurse on each deepest unfinished goal; run hammer and whole-proof sampling there; splice successful replacements into the parent; repeat until no admits remain or budgets are exhausted. Inference: in Verus, recurse on individual verification conditions, loop-invariant obligations, or failed lemma calls, carrying the verified Rust context into each prompt. The final acceptance condition must be a complete verus run, so an LLM’s unsound intermediate reasoning cannot weaken soundness.

external information and evaluation evidence

Cobblestone exposes two useful inputs. A perfect-premises oracle supplies lemmas used by the human proof; a perfect-decomposition oracle supplies a human proof prefix that splits the theorem. Together the variants proved 58% of CoqGym100 and 55% of Wigderson100 (Figure 13, p. 713). The paper reports baseline fractions on the same subsets: CoqHammer 30% and 27%, a chain-of-thought baseline 25% and 19%, and automatic Cobblestone 48% and 38% (Sec. 1, p. 705; Figure 7, p. 711). The text of Sec. 3.5 (p. 713) states the combined figures the other way round (“55% of CoqGym100 and 58% of Wigderson100”), but Figure 13, the abstract and the introduction give 58% for CoqGym100 and 55% for Wigderson100, which is what is used here. It also reports 44/48 (91.6%) CoqGym100 theorems within one invocation and four more by recursion, and 31/38 (81%) Wigderson100 within one invocation and seven more by recursion (Sec. 3.4, p. 712). Denominators and dataset names are retained because these percentages are not interchangeable.

Failures expose limits: “Cobblestone and its variants cannot prove 45 theorems from Wigderson100 and 42 from CoqGym100”; of 14 such theorems sampled for manual study, 5 have human-written proofs of 20+ tactics, and some theorems make partial progress difficult because their ground-truth proofs use tactics like unfold and apply without decomposing the goal (Sec. 3.6, p. 713). Sec. 3.7 (p. 714) cautions that the oracle results do not indicate how an interactive, semi-automated approach would perform. Inference: they are upper-bound style evidence because the “perfect” information comes from human-written proofs.

trust, assumptions, and VL threat

The LLM is not trusted: the abstract says the final proof is “guaranteed to be sound, despite the reliance on unsound LLMs”, and Cobblestone returns a proof only after executing it in Coq (Sec. 2.5). Inference: the trusted components then include Coq’s checker, CoqHammer’s proof reconstruction when it is accepted, and the benchmark’s theorem statements and libraries; the paper does not list a trusted base. The paper argues that all proofs can be expressed as a prefix followed by bullet subproofs (Sec. 2.5, p. 708), but the method gains most when subgoal decomposition exposes reusable progress. It does not establish that an LLM understands Rust, Verus, unsafe code, or temporal properties.

Inference: Cobblestone is a high threat to a VL workflow that asks an agent for one monolithic Verus proof and discards intermediate failures; recursive reuse of verified partial progress is directly applicable. It is a lower threat to Verus’s soundness because the verifier remains the final checker. VL should not redo Coq-specific bullet parsing, but should investigate verifier-diagnostic localization, bounded recursive prompting, and premise/decomposition retrieval. The reported benchmarks are small 100-theorem samples and use Coq; they do not measure product-scale Rust verification.

techniques for the catalog

• hammer-first synthesis — try automated theorem proving globally and again on each unfinished subgoal
• structured whole-proof prompting — provide theorem state, definitions, context, and prior lemmas to an LLM sampling complete scripts
• fail-safe localization — execute nested proof structure while replacing failing suffixes with temporary admits
• recursive divide and conquer — preserve verified subproofs and recursively repair only deepest unfinished goals
• premise and decomposition oracles — supply relevant lemmas or a goal-splitting prefix as external guidance Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Since Cobblestone uses an LLM as a black box, it works with any LLM that supports tool use.”): read the whole paper text (references skimmed) and checked every quotation, number, section and page reference and the technique steps against it; changed the page and section references that were off (Sec. 2 to Sec. 1, Sec. 3.3 to Sec. 3.4, pp. 708-709 to p. 709), the description of the two fail-safe complications, the recursion call arguments, the failure-count wording (variants, 14 sampled theorems), and the trust section; added the per-dataset cost, setup numbers and a note that Sec. 3.5 text swaps the 58%/55% figures; labelled my own conclusions as Inference. Not checked: the Verus transfer claims (my inferences, not in the paper), the replication package, the references list, and figure pixel details beyond the numbers in the text layer.

Last edited: 2026-10-17