Outcome Logic

Origin. Zilberstein and colleagues introduced Outcome Logic (2023). Unifies Hoare logic (over-approximate) and incorrectness logic (under-approximate). Both forward and backward reasoning. Hyperproperty reasoning about sets of traces. Modern framework for program verification.

Models. Unified verification framework. Hoare: all executions from P reach Q (over-approximate). Incorrectness: some execution reaches bad state (under-approximate). Outcome: relate input sets to output sets with both. Hyper-triples reason about trace sets.

Formalism.

Outcome triple: [P] C [Q, R]

Meaning: starting from states in P, executing C:

Q describes possible outcomes (over-approximate: must end in Q)
R describes definite outcomes (under-approximate: will end in R)

Special cases:

[P] C [Q, ∅]: pure over-approximation (Hoare-style)
[P] C [⊤, R]: pure under-approximation (incorrectness-style)

Hyper-triples: Relate sets of executions, not just individual states. Express information flow, non-interference.

Rules: Sequential composition: [P] C₁ [Q₁, R₁] [Q₁] C₂ [Q₂, R₂] ───────────────────────────────────── [P] C₁;C₂ [Q₂, R₁ ∧ R₂ appropriate]

Frame rule (extends): [P] C [Q, R] ───────────────────────── [P * F] C [Q * F, R * F]

Bi-abduction: Find frame and anti-frame simultaneously. Synthesize specifications.

Symbols.

Symbol	Unicode	Name	Meaning
[P]C[Q,R]	—	Outcome triple	Unified spec
Q	—	Over-approx	Must reach
R	—	Under-approx	Will reach
*	—	Separating conj	Disjoint
—*	—	Magic wand	Frame
⊤	U+22A4	True	Any state

Metatheory. Generalizes both Hoare and incorrectness logic. Sound for appropriate semantics. Compositional reasoning preserved. Connects to hyper Hoare logic. Under development. Practical tools emerging.

Applies to. Program verification (unified). Bug finding with guarantees. Security (information flow). Compiler correctness. Compositional verification. Specification synthesis.

Limitations. Recent — less mature. Tool support developing. Specification burden. Complexity of hyper-reasoning. Learning both over and under approximation. Theory still evolving.