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. Recent, and the tooling is behind the theory. Outcome assertions are harder to write than state assertions, and the monoidal structure has to be chosen correctly for the effect at hand. Loops need the indexed families that For consumes, not single invariants. The BI layer over collections adds a proof burden that plain Hoare reasoning does not carry.

© 2026 Lingenic LLC