Reference. Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary

Hanxi Chen, Noam Zilberstein, Andrew C. Myers, Alexandra Silva · arXiv · 2026 · probabilistic outcome-logic · arXiv
In the context of probabilistic programs, an oblivious adversary resolves nondeterminism without seeing the outcomes of random draws. Obliviousness is a common assumption in online algorithms and distributed protocols, but the complex interaction between random draws and adversarial choices makes it challenging to reason about correctness. While there has been significant progress toward reasoning about programs that combine randomization with nondeterminism, most of the work has focused on the adaptive model, whose omniscient view of program state is too powerful to establish correctness for certain classes of programs. We introduce Oblivious Probabilistic Outcome Logic (opOL), a new logic for reasoning about probabilistic programs with nondeterminism controlled by an oblivious adversary. Building on Outcome Logic and Probabilistic Separation Logic, opOL models adversarial choice as a resource and uses probabilistic independence to ensure that random outcomes are hidden from the adversary. The opOL proof system provides expressive and compositional rules for case analysis on both random and nondeterministic outcomes, and for proving almost-sure termination. Expressivity is tested through several case studies, including a paging algorithm and a leader election protocol. The opOL metatheory and case studies are mechanized in Lean 4.

Cite
Cite as @chen-2026-oblivious (helia, typst) · \cite{chen-2026-oblivious} (LaTeX)
BibTeX
bibtex · 8 lines
@misc{chen-2026-oblivious,
  author = {Hanxi Chen and Noam Zilberstein and Andrew C. Myers and Alexandra Silva},
  title = {Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary},
  year = {2026},
  month = {7},
  eprint = {2607.16533},
  archiveprefix = {arXiv}
}
hayagriva YAML (typst)
yaml · 11 lines
chen-2026-oblivious:
  type: misc
  title: 'Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary'
  author:
  - Chen, Hanxi
  - Zilberstein, Noam
  - Myers, Andrew C.
  - Silva, Alexandra
  date: 2026-07
  serial-number:
    arxiv: '2607.16533'
Download: chen-2026-oblivious.bib · chen-2026-oblivious.yml
Cites 47 works (8 here)
With notes (8)

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants zilberstein-2026-probabilisticPOPL · 2026
Although randomization has long been used in distributed computing, formal methods for reasoning aboutprobabilistic concurrent programs have lagged behind. No existing program logics can express specificationsabout the full distributions of outcomes resulting from programs that are both probabilistic and concurrent. To address this, we introduce Probabilistic Concurrent Outcome Logic ( pcOL ), which incorporates ideas fromconcurrent and probabilistic separation logics into Outcome Logic to introduce new compositional reasoningprinciples. At its core, pcOL reinterprets the rules of Concurrent Separation Logic in a setting where separationmodels probabilistic independence, so as to compositionally describe joint distributions over variables inconcurrent threads. Reasoning about outcomes also proves crucial, as case analysis is often necessary to deriveprecise information about threads that rely on randomized shared state. We demonstrate pcOL on a variety ofexamples, including to prove almost sure termination of unbounded loops.
PDF · DOI · arXiv · pldb

A Demonic Outcome Logic for Randomized Nondeterminism zilberstein-2025-aPOPL · 2025
Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but there is a gap when programs also exploit nondeterminism(for concurrency, efficiency, or algorithmic design). In this paper, we introduce Demonic Outcome Logic for reasoning about programs that exploit both randomization and nondeterminism. The logic includes several novel features, such as reasoning about multiple executions in tandem and manipulating pre- and postconditions using familiar equational laws—including the distributive law of probabilistic choices over nondeterministic ones. We also give rules for loops that both establish termination and quantify the distribution of final outcomes from a single premise. We illustrate the reasoning capabilities of Demonic Outcome Logic through several case studies, including the Monty Hall problem, an adversarial protocol for simulating fair coins, and a heuristic based probabilistic SAT solver.
PDF · DOI · arXiv · pldb

Denotational Semantics for Probabilistic and Concurrent Programs zilberstein-2025-denotationalCONCUR · 2025
We develop a denotational model for probabilistic and concurrent imperative programs, a class of programs with standard control flow via conditionals and while-loops, as well as probabilistic actions and parallel composition. Whereas semantics for concurrent or randomized programs in isolation is well studied, their combination has not been thoroughly explored and presents unique challenges. The crux of the problem is that interactions between control flow, probabilistic actions, and concurrent execution cannot be captured by straightforward generalizations of prior work on pomsets and convex languages, prominent models for those effects, individually. Our model has good domain theoretic properties, important for semantics of unbounded loops. We also prove two adequacy theorems, showing that the model subsumes typical powerdomain semantics for concurrency and convex powerdomain semantics for probabilistic nondeterminism.
DOI · arXiv

Lilac: A Modal Separation Logic for Conditional Probability li-2023-lilacPLDI · 2023
We present Lilac, a separation logic for reasoning about probabilistic programs where separating conjunction captures probabilistic independence. Inspired by an analogy with mutable state where sampling corresponds to dynamic allocation, we show how probability spaces over a fixed, ambient sample space appear to be the natural analogue of heap fragments, and present a new combining operation on them such that probability spaces behave like heaps and measurability of random variables behaves like ownership. This combining operation forms the basis for our model of separation, and produces a logic with many pleasant properties. In particular, Lilac has a frame rule identical to the ordinary one, and naturally accommodates advanced features like continuous random variables and reasoning about quantitative properties of programs. Then we propose a new modality based on disintegration theory for reasoning about conditional probability. We show how the resulting modal logic validates examples from prior work, and give a formal verification of an intricate weighted sampling algorithm whose correctness depends crucially on conditional independence structure.
PDF · DOI · arXiv · pldb

Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning zilberstein-2023-outcomeOOPSLA · 2023
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory can be used for both correctness and incorrectness reasoning. We present Outcome Logic (OL), a novel generalization of Hoare Logic that is both monadic (to capture computational effects) and monoidal (to reason about outcomes and reachability). OL expresses true positive bugs, while retaining correctness reasoning abilities as well. To formalize the applicability of OL to both correctness and incorrectness, we prove that any false OL specification can be disproven in OL itself. We also use our framework to reason about new types of incorrectness in nondeterministic and probabilistic programs. Given these advances, we advocate for OL as a new foundational theory of correctness and incorrectness.
PDF · DOI · arXiv · pldb

Iris from the ground up: A modular foundation for higher-order concurrent separation logic jung_etal_iris_ground_up_2018JFP · 2018
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.
PDF · DOI · pldb

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning jung-2015-irisPOPL · 2015
PDF · DOI · pldb

Separation logic: A logic for shared mutable data structures reynolds_separation_2002LICS · 2002
In joint work with Peter O’Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a “separating conjunction” that asserts that its subformulas hold for disjoint parts of the heap, and a closely related “separating implication”. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions.
DOI
External (39)
chen-2026-oblivious reference entries/refs/chen-2026-oblivious/chen-2026-oblivious.hel