Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary
Hanxi Chen, Noam Zilberstein, Andrew C. Myers, Alexandra Silva
cs.PL
Jul 17, 2026 · v1
cs.LO
TL;DR
The opOL metatheory and case studies are mechanized in Lean 4.
Abstract
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.
Problem
Reasoning about probabilistic programs whose nondeterminism is resolved by an oblivious adversary (one who cannot observe random draw outcomes) is difficult because existing work targets the more powerful adaptive adversary model, which is too strong for certain correctness properties.
Approach
Oblivious Probabilistic Outcome Logic (opOL) is introduced, building on Outcome Logic and Probabilistic Separation Logic. Adversarial choice is modeled as a resource and probabilistic independence ensures random outcomes remain hidden from the adversary. The proof system offers compositional rules for case analysis over random and nondeterministic outcomes and for proving almost-sure termination. The metatheory and case studies are mechanized in Lean 4.
Results
The logic's expressivity is demonstrated through case studies including a paging algorithm and a leader election protocol, all mechanized in Lean 4.
