Outcome Logic

Origin. Noam Zilberstein, Derek Dreyer, and Alexandra Silva, "Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning" (OOPSLA 2023; PACMPL 7(OOPSLA1):522–550; arXiv:2303.03111). Continued in outcome separation logic (Zilberstein, Saliling, Silva 2024), demonic outcome logic (Zilberstein, Kozen, Silva, Tassarotti 2025), and a general metatheory for branching effects (Zilberstein, TOPLAS 2025).

Models. Two generalizations of Hoare logic at once. Monadic: a command takes a state to a collection of outcomes in some monad, so nondeterminism, probability, and failure are all covered by choosing the monad. Monoidal: assertions are satisfied by a whole collection of outcomes rather than by one state, and a BI-style separating conjunction ⊕ splits that collection. The diagnosis driving the design is that incorrectness logic conflates two things — reachability and under-approximation — which Outcome Logic separates: ⊕ expresses reachability, and under-approximation comes from dropping outcomes.

Formalism.

Triples: ⟨φ⟩ C ⟨ψ⟩ φ and ψ are outcome assertions, satisfied by a monoidal collection of outcomes. Individual outcomes are written P, Q; as in incorrectness logic, (ok : P) and (er : P) distinguish successful from failed termination, but here they are ordinary assertions rather than part of the triple.

Outcome conjunction: φ ⊕ ψ: the collection splits into one part satisfying φ and one satisfying ψ. This is separation over outcomes, not over the heap — a BI instance on the frame of collections. Asserting φ ⊕ ψ asserts that both branches are reached; it is the reachability connective.

Recovering the two classical logics: ⟨P⟩ C ⟨Q⟩ with a single outcome is Hoare logic. ⟨P⟩ C ⟨⊤ ⊕ Q⟩ is incorrectness logic: Q is reached, and ⊤ absorbs whatever else happens. Under-approximation is then the act of weakening some outcome to ⊤, which is why it is independent of ⊕.

Rules:

⟨φ⟩ C₁ ⟨ψ⟩ ⟨ψ⟩ C₂ ⟨ϑ⟩ ───────────────────────── (Seq) ⟨φ⟩ C₁ ⨟ C₂ ⟨ϑ⟩

Sequencing keeps the ordinary Hoare shape — the generalization is in the assertions, not in the composition.

⟨φ₁⟩ C ⟨ψ₁⟩ ⟨φ₂⟩ C ⟨ψ₂⟩ ───────────────────────────── (Split) ⟨φ₁ ⊕ φ₂⟩ C ⟨ψ₁ ⊕ ψ₂⟩

Split is where ⊕ does the work: reason about each branch separately, then recombine.

φ′ ⇒ φ ⟨φ⟩ C ⟨ψ⟩ ψ ⇒ ψ′ ───────────────────────────────── (Consequence) ⟨φ′⟩ C ⟨ψ′⟩

∀i ∈ ℕ. ⟨φᵢ⟩ C ⟨φᵢ₊₁⟩ ────────────────────────── (For) ⟨φ₀⟩ for N do C ⟨φ_N⟩

Outcome dropping: assume e does nothing when e holds and eliminates the current outcome otherwise. This is the syntactic form of under-approximation: forget the outcomes you do not wish to reason about.

Symbols.

Metatheory. The unification is genuine rather than a juxtaposition: Hoare logic and incorrectness logic are both instances, obtained by choice of assertion shape, not by choice of proof system. Bugs proved are true bugs, and correctness reasoning is not surrendered to get that. The sharpest result is that any false Outcome Logic specification can be disproven in Outcome Logic itself — the logic is closed under refutation, which neither Hoare nor incorrectness logic manages alone. The monadic parametrization means one metatheory covers nondeterministic, probabilistic, and demonic branching; the TOPLAS 2025 paper carries this out in full generality.

Applies to. Unified correctness and bug-finding. Probabilistic program reasoning, by taking the distribution monad. Nondeterministic and demonic branching. Local reasoning about effects, via outcome separation logic. Concurrency with probabilistic independence and conditioning.

Limitations. The framework is parameterized by a monad, and monads do not compose: there is no distributive law between the powerset and distribution monads, so an instantiation covering probabilistic and nondeterministic choice at once is not obtained by combining the two instantiations, and each such combination is a separate construction. Iteration is handled by the For rule, which consumes an ℕ-indexed family φᵢ rather than a single invariant, so unbounded loops require an assertion for every iteration count and the family's existence is subject to the same expressibility hypothesis Cook identified. Under-approximation is achieved by weakening an outcome to ⊤, and a triple that has done so asserts nothing whatever about the discarded outcomes — the strength of ⊕ does not recover them. Outcome assertions are satisfied by collections and their entailment includes arbitrary state entailment, so the consequence rule needs the same undecidable oracle. The triples quantify over the outcomes of a single initial state, so relational properties of two separate executions are not outcome assertions.

© 2026 Lingenic LLC