Scenario Proofs for Verification of Distributed Protocols

Zhendong Ang; George Pîrlea; Umang Mathur

Home/Archive/arXiv

arXiv · 2610.15408

Scenario Proofs for Verification of Distributed Protocols

Zhendong Ang·George Pîrlea·Umang Mathur

View original source ↗Read source document ↗Export metadata ↓

Abstract

Formal verification of distributed protocols is still dominated by inductive-invariant proofs, whose central challenge is discovering strengthening assertions that rule out unreachable states. This burden is often misaligned with how protocol designers reason: they explain correctness by following representative executions, causal histories, and phase-structured interactions among nodes. This paper introduces scenario proofs, a verification methodology that makes such execution-oriented reasoning formal. A scenario is a structured expression describing representative protocol executions, enriched with ghost variables. Rather than enumerate all possible interleavings, a scenario describes canonical executions and uses a sound semi-commutation relation to account for reorderings that preserve feasibility and final states. Verification then factors into two main obligations. Coverage shows that every feasible protocol execution is equivalent, up to semi-commutation, to one described by the scenario; this obligation is independent of the safety property and serves as a reusable behavioral characterization of the protocol. Correctness proves the desired safety property only over the representative executions, using Hoare-style weakest-precondition reasoning along the scenario structure. We formalize the scenario language, its layered semantics, and proof rules for coverage and correctness. Through case studies of ring leader election, two-phase commit, a decentralized lock, two variants of multi-signature payment, and single-decree Paxos, we show how scenario proofs capture the causal and phase-based arguments used informally by protocol designers. These examples illustrate that scenario proofs can replace monolithic invariant discovery with structured reasoning over representative executions, while retaining a rigorous connection to all feasible protocol behaviors.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Zhendong Ang, George Pîrlea, Umang Mathur. 2026-10-11. Scenario Proofs for Verification of Distributed Protocols. https://arxiv.org/abs/2610.15408

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

KEEP EXPLORING

Related papers

arXiv2026

FlowBook: Enforcing Reproducibility in Computational Notebooks

Computational notebooks interleave code cells with their outputs and let users edit and execute cells in arbitrary order. This flexibility supports interactive exploration, but it also allows outputs to become inconsistent with the notebook's current code and data. Such inconsistencies can lead users to draw invalid scientific conclusions. We argue that notebooks should always be output consistent: every output should match what a top-to-bottom execution of the current code would produce. Forcing a top-to-bottom execution after each edit would guarantee this, but at prohibitive cost: such an execution can take minutes to hours. We present FlowBook, a dynamic analysis for Python notebooks that enforces output consistency without giving up out-of-order execution. FlowBook does this by enforcing a stronger property, rerun consistency: no location read by a cell may be written by any cell below it. Rerun consistency guarantees that rerunning a cell later, in any order, reproduces its current output. FlowBook tracks each cell's read and write sets at cell boundaries, blocks updates that would violate rerun consistency, and marks as stale any cell whose inputs may have changed. We prove that a notebook with no stale cells is both rerun and output consistent. Users remain free to execute cells in arbitrary order; the only restriction is that recorded outputs may not silently depend on the order in which cells were executed. Across 61 real-world notebooks, FlowBook flagged 203 rerun-inconsistent cells. Rerunning 62% led to output inconsistencies. A further 21% change notebook state with no visible output, which can affect the results of later edits and reruns; only 5% are false positives of FlowBook's conservative analysis. FlowBook's AI repair agent repaired all 203 cells with local edits and no human intervention. FlowBook's median overhead is only 26 ms per cell execution.

cs.PL↗

arXiv2026

From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware

Enforcing invariants in safety-critical firmware is increasingly urgent as generated code becomes widespread, but standard extraction targets for proof assistants require runtimes too large for many embedded devices. We present a pipeline for running formally verified Rocq firmware logic on Cortex-M microcontrollers. The pipeline extracts Gallina to Scheme, compiles it with Encore!, a bare-metal Continuation-Passing Style (CPS) bytecode virtual machine, and embeds the result in no_std Rust firmware. We structure applications as pure state-transition functions, so the business logic is proved in Rocq while the event/effect boundary, host callbacks, compiler, and VM remain explicit trusted components: no proof yet relates bytecode execution to Gallina semantics. On eight firmware workloads, from APDU parsing to a credential store, Encore! runs unmodified Rocq-extracted code within the 50 KiB RAM budget of ST33-class targets on every input size, where CertiRocq's generated code runs out of memory on the larger ones, at the price of up to 10 times more executed instructions than CertiRocq; a transaction-signing application is validated on physical Ledger Flex hardware.

cs.PL↗

arXiv2026

Compositional Information Geometry of Probabilistic Programs

We study the compositional, intensional information geometry of probabilistic programs. For a first-order probabilistic programming language with finite random variables, we construct a contravariant lax monoidal functor that, for a program of type $X \to Y$, pulls back a (degenerate) Riemannian metric on $Y$ to $X$. It specialises to the Fisher metric in the case of standard statistical models and to ordinary pullback in the case of deterministic programs. We further justify this construction in two ways. First, we show that this functor arises as a pullback of geometry from a universal space of programs over a type $Y$ with a fixed trace space. Second, we show that it is a special case of a more general pullback construction over weighted measures. Our compositional geometry depends on the presentation of the program, and we study how it relates to the (non-compositional) geometry of the realised measures by establishing a three-level inequality relating our score-velocity metric for the program, the program's corresponding output-conditioned metric, and the standard Wasserstein-Fisher-Rao metric of the realised family. Finally, we show how the theory can be extended to accommodate continuous random variables using diffeological quasi-Borel spaces. We also discuss several concrete directions for future work.

cs.PL↗