Source-linked AI summary
Synthesizing Proofs Using Proof Sharding and Exploration
Seyed Armin Vakil Ghahani, Manos Kapritsos
TL;DR
Formal verification offers strong correctness guarantees for distributed systems, but programmers must repeatedly add annotations because theorem provers do not guide the next proof step. ProofSaX decomposes lemmas into smaller obligations, explores annotations for failing shards, and restricts synthesis to common patterns that help the prover make progress. ProofSaX found proofs of correctness in 86 out of 103 cases, with execution times ranging from one minute to two hours.
Problem
Formal verification offers strong correctness guarantees for distributed systems, but programmers must repeatedly add annotations because theorem provers do not guide the next proof step.
Source: §1 · p. 1Method
ProofSaX decomposes lemmas into smaller obligations, explores annotations for failing shards, and restricts synthesis to common patterns that help the prover make progress.
Source: §1 · p. 2Results
ProofSaX found proofs of correctness in 86 out of 103 cases, with execution times ranging from one minute to two hours.
Source: §9 · p. 13Takeaways & Limitations
ProofSaX can find proofs for complex distributed systems when each shard requires only a few proof annotations.
Source: §9 · p. 13ProofSaX does not synthesize if conditions outside its supported proof-annotation patterns, so proofs requiring those constructs may remain incomplete.
Source: §6.3 · p. 11
Abstract
from arXiv · showhide
Distributed systems are hard to implement correctly, and subtle bugs can go undetected using traditional testing. Formal verification offers an alternative for proving the correctness of complex distributed systems. Despite previous efforts to automate and facilitate formal verification, it is still hard to integrate formal verification in software development. Programmers need to query the theorem prover repeatedly to find the correct proof of their system. This cycle of going back and forth with the theorem prover involves a lot of human intervention and is a barrier to adopting formal verification in software development. In this paper, we address the challenges of scaling formal verification in practice by reducing the human intervention required to find the correctness proof of a distributed system. We propose ProofSaX, an automated tool that shards large verification tasks and explores the proof search space for each shard independently to synthesize correctness proofs. We use controlled exploration when adding possible proof annotations to handle the search-space explosion problem. We evaluate ProofSaX on a variety of safety proofs for distributed systems. We show that ProofSaX can find the last proof annotation in 86 out of 103 proof-completion tasks, with runtimes ranging from one minute to two hours.
1 Introduction
ProofSaX targets the human effort of proof debugging by automating annotation search, while acknowledging that finding every proof is undecidable. It shards proof obligations, explores likely annotations, and completes many distributed-systems proofs.
1 Introduction
- Formal verification can provide strong correctness guarantees, but writing proofs is costly and theorem provers leave programmers to choose annotations after failures.Source: §1 · p. 1
- ProofPlumber automates annotation generation but leaves developers to choose what to try; ProofSaX automates iterative prover queries and annotation generation to reduce manual input.Source: §1 · p. 1
- ProofSaX divides verification tasks into smaller proof obligations and explores annotations only for obligations the prover cannot prove independently.Source: §1 · p. 2
- Rather than enumerate every annotation, ProofSaX synthesizes common programmer-used patterns that help the prover make progress, keeping search tractable.Source: §1 · p. 2
- Candidate annotations are checked in parallel using multiple prover instances, reducing lemma-proof execution from multiple hours to a few minutes.Source: §1 · p. 2
- 86 out of 103 experiments were completed in one minute to two hours, while leader-election proofs were found automatically in under two minutes.Source: §1 · p. 2
2 Background: Writing Proofs Manually
The section explains how programmers prove safety inductively and why completing those proofs often requires manual annotation and repeated theorem-prover interaction.
2 Background: Writing Proofs Manually
- Safety proofs establish an inductive invariant that holds initially and is preserved by every valid transition.The Library example’s invariant states that each patron has at most one book.Source: §2 · pp. 2–3
- After a proof failure, the prover may identify only an unproved postcondition, leaving programmers to diagnose the cause and add annotations manually.The programmer then queries the prover again to check whether the annotation completes the proof.Source: §2 · p. 3
2.1.1 Introducing new variables.
- Expanding Next exposes transition cases, while expanding Safety(s') introduces name; programmers cannot know which route is better and must explore both.Expanding the transition cases can let programmers focus only on the cases requiring further annotations.Source: §2.1.1 · pp. 3–4
2.1.2 Triggers.
- For quantifiers, programmers must invoke matching triggers with bound variables; needed invocations can depend on introduced variables and combining annotations in the right order.The Library example’s table lists prover-selected trigger sets, and invoking HasAtMostOneBook(s, name) lets the prover conclude the safety lemma.Source: Table 1 · p. 3, §2.1.2 · p. 4
3 Narrow & Explore
ProofSaX addresses unbounded annotation search with Narrow and Explore: it breaks verification tasks into smaller cases, then searches each shard in a controlled way.
3 Narrow & Explore
- Narrowing shrinks proof obligations into smaller, independent cases that require fewer and simpler annotations.The design follows programmers’ practice of narrowing proof scope and exploring each scope.Source: §3 · p. 4, Narrow · p. 5
Explore.
- Explore searches each shard for annotations that help the prover make progress, avoiding patterns that cannot change its behavior.For example, generating expressions that are not triggers for any program quantifier is pointless.Source: Explore · p. 5
3 Narrow & Explore
- ProofSaX’s Narrow and Explore components break large verification tasks into smaller pieces and control annotation search for each piece.A naive approach that adds annotations one by one is not scalable because the possible annotations are unbounded.Source: §3 · pp. 4–5, Explore · p. 5
4 ProofSaX
ProofSaX combines proof sharding with lemma transformers that explore proof annotations, checking generated candidates with the theorem prover and refining failing obligations. Its transformers control expression and trigger search, invoke helper lemmas, reveal definitions, shard conditions, and introduce quantified variables.
4 ProofSaX
- ProofSaX decomposes failing lemmas into smaller obligations and applies transformers to generate candidate proofs, which the theorem prover checks before further refinement.The system returns a passing proof when it finds one; otherwise, it recursively refines the failing lemma.Source: §4 · p. 5, Figure 3 · p. 5
4.1 Controlled Expression Synthesizer
- Expression complexity bounds synthesis by counting operands and variables, while ExprGenerator builds expressions recursively from in-scope variables and smaller expressions.Unary and binary operations, collection indexing, datatype access, and function calls each add complexity according to their structure.Source: §4.1 · pp. 5–6
4.2 Trigger Synthesizer Transformer
- ProofSaX generates expressions matching quantifier triggers at increasing complexity, then checks trigger invocations in batches of 64 and tests pairs of triggers.The batch size is an empirically derived happy medium; a precomputed covering ensures every pair appears in at least one batch.Source: §4.2 · pp. 6–7
4.3 Lemma Invocation Transformer
- The lemma invocation transformer generates calls to helper lemmas available at the failure point, creating a candidate lemma for each invocation.It avoids introducing loops in the function-call graph and stops checking remaining candidates after one passes.Source: §4.3 · p. 7
4.4 Reveal Transformer
- The Reveal Transformer automatically reveals definitions that programmers may otherwise expose manually when hidden definitions impede proof checking.The prover can expand definitions by default, but irrelevant expansions may cause search-space explosion.Source: §4.4 · p. 7
4.5 Pre/Post-condition Sharder
- For disjunctive preconditions, ProofSaX generates a lemma for each case and preserves the original proof so already-proven cases can pass without further exploration.It then focuses exploration on the cases that fail.Source: §4.5 · pp. 7–8
- For conjunctive postconditions, ProofSaX creates a lemma per conjunct, carries earlier conjuncts as preconditions, and uses contradiction to reuse the original proof.If the original body asserts both conjuncts, sharding may still require proving both.Source: §4.5 · p. 8
4.6 Quantifier Elimination Transformer
- The quantifier elimination transformer introduces variables from existential preconditions or universal postconditions so exploration transformers can use them in the proof search.Source: §4.6 · p. 8
5 Proving Lemmas at Scale
ProofSaX extends Dafny to analyze lemmas and explore proof annotations, while a parallel theorem-prover backend checks generated lemmas at scale. Its output remains verifiable by unmodified Dafny and does not increase the trusted computing base.
5 Proving Lemmas at Scale
- ProofSaX extends Dafny and uses its abstract syntax tree to analyze programs and explore proof search by adding annotations and querying the prover.Upon finding a correct proof, ProofSaX displays it to the user.Source: §5 · pp. 8–9
- The generated Dafny proof can be checked with unmodified Dafny, so ProofSaX does not increase the trusted computing base.Source: §5 · p. 9
- A parallel C++ backend checks generated lemmas across cluster nodes, with requests distributed by round-robin scheduling over gRPC.Each backend instance can use all cores on its machine.Source: §5 · p. 9
6 Evaluation
ProofSaX is evaluated on proof-completion tasks with one or multiple removed annotations, as well as from-scratch proofs and a backend scalability experiment. Results show successes across these settings, with outcomes bounded by annotation complexity, supported patterns, and sharding.
6.1 ProofSaX Finding Single Holes
- 86 of 103 single-hole experiments were completed after removing a proof annotation from a published proof.The benchmark table reports per-benchmark experiment and success counts.Source: §6.1 · p. 10, Table 4 · p. 10
- The 17 single-hole failures mainly involved high-complexity missing annotations or unsupported features such as templates and set comprehensions.Figure 6 groups the experiments and successes by expression-complexity level.Source: Figure 6 · p. 9, §6.1 · p. 10
- For successful single-hole experiments, ProofSaX found the missing proof within 20 minutes except for a few Paxos edge cases.Figure 7 presents execution times for successful cases.Source: Figure 7 · p. 9, §6.1 · p. 10
- Each experiment used one or more lemma transformers, and Table 5 reports how many experiments each transformer type helped solve.Source: §6.1 · p. 10, Table 5 · p. 10
6.2 Multi-hole Experiments
- 32 of 42 multi-hole experiments were solved, but these experiments included only cases whose corresponding single-hole versions ProofSaX could solve.Seven of the ten failures required two lemma invocations, which ProofSaX does not synthesize because that would cause search-space explosion.Source: §6.2 · p. 10
6.3 Finding Proofs from Scratch
- After removing all manually written proof annotations from each lemma across the Table 4 benchmarks, ProofSaX found proofs from scratch in eight of 49 experiments, with one experiment per lemma.In the single-hole experiments, ProofSaX also found proofs for the first and last lemmas from empty bodies in 148 and 75 seconds, respectively.Source: §6.3 · p. 11
- ProofSaX did not find the Ring proof’s second lemma within two hours after checking 235,000 lemmas; it does not synthesize if-conditions outside its supported annotation patterns.The account also notes that ProofSaX does not synthesize helper lemmas on its own, so needed helper-lemma signatures must already be available.Source: §6.3 · p. 11
6.4 ProofSaX Scalability
- With ten backend nodes, the missing annotation was found in under 25 minutes, compared with over six hours using one node.The experiment generated 52K lemmas with one node and 38K with ten nodes.Source: §6.4 · p. 12, Figure 8 · p. 12
7 Discussion
ProofSaX’s divide principle addresses proof-debugging cases where prover timeouts provide no insight into which obligation needs annotations. The authors also describe how trigger-using languages beyond Dafny could apply the techniques to synthesize trigger invocations.
7.1 Timeouts
- When a prover times out without identifying the obligation needing annotations, ProofSaX’s divide principle helps developers split the proof and find proofs for individual parts independently.Source: §7.1 · p. 12
7.2 Trigger-based Programming Languages
- F* and Verus are identified as possible beneficiaries because they use Z3 and triggers to instantiate quantifiers, like Dafny.The proposed application is synthesizing trigger invocations.Source: §7.2 · p. 12
8 Related Work
Prior automation has addressed invariant discovery and proof assistance, but cited approaches still leave developers responsible for some proof obligations or next steps. ProofSaX complements these efforts by automating proof finding through sharding, while LLM-based synthesis is noted as a possible future direction.
Related work on distributed systems verification
- Earlier distributed-systems tools automated invariant discovery, but developers still had to prove candidate invariants inductive; ProofSaX complements them with proof finding through sharding.Earlier work included methods restricted to EPR and later work for complex protocols using undecidable logic.Source: §8 · p. 12
Interactive theorem provers and automated code manipulations
- CoqHammer, SledgeHammer, and ProofPlumber speed proof-debugging steps, but developers still choose the annotation or tactic to try after failure.Source: §8 · p. 12
Large Language Models
- LLM proof synthesis for Dafny and Verus is described as promising future work for distributed-systems proofs, while the authors favor first studying requirements with conventional methods.They identify holes per shard as one factor relevant to scalability.Source: §8 · pp. 12–13
9 Conclusion
ProofSaX shards proof obligations where possible and explores each shard independently. It finds proofs in 86 of 103 cases, with execution times from one minute to two hours.
9 Conclusion
- 86 out of 103 cases yielded proofs, with execution times ranging from one minute to two hours.The reported capability applies to complex distributed systems when each shard requires only a few proof annotations.Source: §9 · p. 13
- ProofSaX breaks down proof obligations into shards where possible and explores each shard’s proof-search space independently.The approach is described as controlled proof search for synthesizing correctness proofs.Source: §9 · p. 13
- A parallel theorem-prover backend is used to scale verification of large proofs.Source: §9 · p. 13