While there is a long tradition of reasoning about termination (and nontermination) in the context of program analysis, specialized logics are typically needed to give different termination guarantees. This includes partial correctness, where termination is not guaranteed; total correctness, where it is guaranteed; and newer logics for explicitly proving \emph{nontermination}. We present \emph{Total Outcome Logic}, a single logic which can express the full spectrum of termination conditions and program properties offered by the aforementioned logics.

Total Outcome Logic extends termination and incorrectness reasoning across different kinds of branching effects, so that a single metatheory powers this reasoning in different kinds of programs, including those with nondeterminism and randomization.