Synthesizing Proofs Using Proof Sharding and Exploration

Seyed Armin Vakil Ghahani; Manos Kapritsos

Home/Archive/arXiv

arXiv · 2609.28535

Synthesizing Proofs Using Proof Sharding and Exploration

Seyed Armin Vakil Ghahani·Manos Kapritsos

View original source ↗Read source document ↗Export metadata ↓

Abstract

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.

Explore related subjects

cs.PL cs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Seyed Armin Vakil Ghahani, Manos Kapritsos. 2026-09-22. Synthesizing Proofs Using Proof Sharding and Exploration. https://arxiv.org/abs/2609.28535

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Instrumentation Optimization for Practical Dynamic Race Detection

Dynamic data race detectors are successful at flagging concurrency bugs, but their high runtime overhead limits adoption. This overhead stems primarily from pervasive instrumentation of memory accesses -- a significant fraction of which is for safe accesses. We address this inefficiency through a compiler-integrated approach that identifies safe accesses using static analysis and eliminates instrumentation for these. We strike a careful balance between analysis precision and cost, to ensure applicability to real-world applications. We show that our optimizations never cause ThreadSanitizer to miss races it would otherwise detect. We further observe that many checks are redundant: They only flag a race if a preceding check has already flagged an equivalent race for the same memory location. We show that, when reporting one representative per class is sufficient, even more instrumentation can be eliminated. Lastly, we introduce a dynamic technique that skips instrumentation when there is only one thread at runtime, even when this could not be determined statically. We integrate these static analyses and program transformations into the ThreadSanitizer race detector based on LLVM. Our experiments on a diverse suite of real-world applications, including Memcached, Redis, SQLite, MySQL, and Chromium, demonstrate that our optimizations reduce the number of instrumentation calls at runtime by up to 91% and yield application-level speedups of up to 1.91x, a geometric-mean Chromium speedup of 1.25x on Blink and 1.14x on Speedometer 3.0, and peak speedups reaching 2.28x on Memcached with two server threads. Our optimizations are in the process of being upstreamed into ThreadSanitizer.

cs.PL↗

arXiv2026

A Taxonomy of Predicate Transformer Monads for Specifying Monadic Programs

Monads of weakest precondition predicate transformers are the foundation of several verification frameworks for monadic programs. For specifying monadic computations with nondeterminism and nontermination, in addition to weakest preconditions, we introduce the first strongest postcondition monads covering all combinations of angelic or demonic nondeterminism and partial or total interpretations of nontermination. For extending these base strongest postcondition monads with side effects such as mutable state, monad transformers do not yield the expected monads, so we instead generalize the base monads to arrows and use arrow transformers. We give a taxonomy of weakest precondition and strongest postcondition monads, for the base monads and for their versions with state, and show that the known relationships between under- and over-approximate triples based on predicate transformers already hold at the level of the predicate transformers themselves. We use the predicate transformer monads to define under- and over-approximate triples and, where possible, Dijkstra monads. Finally, we relate these two specification styles.

cs.PL↗

arXiv2026

Compiling Environment Classifiers to Contextual Modal Types

Type systems for metaprogramming take one of two approaches to safeguarding the scopes of variables in generated code. They either use Environment Classifiers (EC) to identify scopes by name (Taha and Nielsen, 2003), or they use Contextual Modal Type Theory (CMTT) to match scopes by structure (Nanevski, Pfenning, and Pientka, 2008). In this paper, we connect these two approaches by compiling a calculus with polymorphic environment classifiers, subtyping, and mutable references to a CMTT-based calculus with polymorphic contexts, mutable references, and first-class substitutions. The key idea is to map each environment classifier to a context. We prove that the compilation preserves types and that compilation preserves the behavior of metaprograms. Both proofs are mechanized in Agda. The compilation shows that CMTT is at least as expressive as environment classifiers. We conjecture that the converse compilation is difficult, because environment classifiers impose a stricter regime on the metaprogram.

cs.PL↗