# 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.

© 2026 Lingenic LLC