Safety-Refined Liveness

by LucTeo on May 10, 2026

Correctness properties of programs are traditionally decomposed into safety (“nothing bad happens”) and liveness (“something good eventually happens”). In sequential verification, this corresponds to the well-known decomposition of total correctness into partial correctness and termination.

In this paper, we present a principle-first view of correctness: under suitable safety guarantees, liveness reduces to a pure progress property. Specifically, if all produced results are correct by construction, then ensuring eventual production of a result is sufficient to guarantee that a correct result is eventually produced.

We formalise this observation in linear temporal logic and show that, under these safety guarantees, eventual correctness reduces to a progress property. A central consequence is conditional compositional correctness: although correctness does not generally compose, it becomes compositional in systems where progress composes under suitable structural conditions.

This reframes compositional reasoning about correctness: under suitable safety guarantees, correctness composes precisely when progress composes.

Introduction

The distinction between safety and liveness is fundamental in reasoning about program correctness. Safety properties constrain the set of admissible executions by excluding undesirable behaviours, while liveness properties ensure that eventually we reach desired results.

In practice, correctness proofs are often structured in two phases:

1. Establish invariants (safety)
2. Prove eventual attainment of the desired outcome (liveness)

This decomposition is standard, yet its consequences are not always fully explored. In particular, we consider the following question:

To what extent can liveness be simplified when safety guarantees are maximal?

We answer this by isolating an explicit principle, often used implicitly in reasoning about programs:

If correctness is enforced by safety, then liveness reduces to progress.

The remainder of the paper formalises and explores this principle, and shows how it enables simplified reasoning about both correctness and compositionality.

Preliminaries

We consider executions as infinite traces over states. We use standard linear temporal logic (LTL) operators:

• $\square P$ — “$P$ holds in all future states”
• $\diamond P$ — “$P$ holds in some future state”

Let:

• $A$ denote the predicate “an answer is produced”
• $G$ denote the predicate “a correct answer is produced”

By definition, $G$ implies $A$.

We assume that $A$ denotes the production of a final observable answer.
We do not reason about intermediate or partial outputs.

We formalise the standard notions of safety and liveness:

Safety (partial correctness): A program is partially correct if all produced answers are correct: $\square(A \Rightarrow G)$

The property $\square(A \Rightarrow G)$ is a safety property: any violation (i.e., producing an incorrect answer) can be detected by observing a finite execution prefix.

Termination (progress): In this setting, termination means that the program eventually produces a final observable answer: $\diamond A$.

Liveness (eventual correctness): We define the property $\diamond G$, meaning that a correct answer is eventually produced. This corresponds to the usual formulation of liveness as “eventually something good happens”.

Progress ($\diamond A$) is a special case of liveness, expressing that some observable outcome eventually occurs.

The property $\diamond A$ is a liveness property: any violation (i.e., the absence of an answer) cannot be established by observing any finite execution prefix.

Notably, these definitions distinguish between:

• producing an answer ($\diamond A$)
• producing a correct answer ($\diamond G$)

The relationship between these will be central to the results that follow.

Informal Principle

The key idea of this paper can be stated informally:

If all produced answers are correct by construction, then eventual correctness (and thus liveness) reduces to progress.

This principle separates correctness obligations (handled by safety) from progress obligations (handled by liveness). In particular, the obligation to prove eventual correctness ($\diamond G$) reduces to proving progress i.e., $\diamond A$.

Example

Consider a concurrent program composed of a finite set of work items. Each work item, when executed, may either produce a result or continue computation. The program completes once some work item produces a final observable answer (after which no further results are possible).

We assume the following:

• Safety (local correctness): Each work item is correct by construction. That is, whenever a work item produces an answer, that answer satisfies the program’s requirements. Formally: $\square(A \Rightarrow G)$
• Progress: The execution model guarantees that a work item capable of producing the final observable answer is eventually executed, and that such execution eventually produces an answer ($\diamond A$).

We want to prove correctness of the program. For that, we need to prove liveness: the program eventually produces a correct answer: $\diamond G$.

In contrast to safety, liveness properties are global. They depend on scheduling, fairness, or termination arguments. Typically, liveness obligations are phrased as ensuring that the correct result is eventually produced ($\diamond G$).

While safety properties can often be established compositionally, liveness typically requires global reasoning.

Using the principle illustrated in this paper, we can reduce this obligation: under $\square(A \Rightarrow G)$, proving $\diamond G$ reduces to proving $\diamond A$, which is ensured by progress.

Once safety properties are established, liveness reasoning simplifies: instead of proving “eventually a correct result is produced”, it suffices to prove termination, i.e., “eventually a result is produced”.

This illustrates a shift in reasoning: correctness is ensured structurally, leaving progress as the only remaining concern.

Safety-Refined Liveness

The following lemma provides a formalisation of the principle stated above.

Lemma (Safety-refined liveness): $\square(A \Rightarrow G) \land \diamond A \Rightarrow \diamond G$.

Proof. From $\diamond A$, there exists a future state in which $A$ holds. From $\square(A \Rightarrow G)$, $G$ must hold in that state. Therefore, $\diamond G$ holds. ∎

The lemma shows that progress implies eventual correctness under safety. We now strengthen this result to an equivalence.

Corollary (Reduction of liveness under safety): Under the assumption $\square(A \Rightarrow G)$ we have $\diamond G \equiv \diamond A$.

Proof. By the lemma, $\diamond A$ implies $\diamond G$ under the assumption $\square(A \Rightarrow G)$. Conversely, $\diamond G$ implies $\diamond A$, since producing a correct answer entails producing an answer. Therefore, under the standing assumption, $\diamond G \equiv \diamond A$. ∎

Interpretation

This result can be understood as a separation of concerns in correctness reasoning.

Under the assumption $\square(A \Rightarrow G)$, all admissible outcomes are correct by construction. As a result, correctness no longer depends on which outcome is produced, but only on whether an outcome is eventually produced.

This shifts the role of liveness: instead of ensuring that a correct result is eventually obtained ($\diamond G$), it suffices to ensure that some result is eventually produced ($\diamond A$).

In this sense, correctness becomes a structural property enforced by safety, while liveness is reduced to a pure progress concern.

Relation to Classical Results

This observation can be seen as a refinement of the classical decomposition:

Total correctness = Partial correctness + Termination

The standard presentation emphasises the separation between partial correctness and termination. In contrast, the emphasis here is on simplifying liveness obligations: instead of proving that a correct result must eventually be produced, we simplify the proof obligation. Under the assumption $\square(A \Rightarrow G)$, it suffices to prove that some result is eventually produced, i.e., termination alone suffices to establish eventual correctness.

In this sense, once partial correctness is ensured, the remaining proof obligation reduces to a progress property.

While this follows from standard theory, it is typically used implicitly rather than stated as an explicit reasoning principle.

Implications for Program Design

The principle suggests a concrete design strategy:

Structure programs so that correctness is enforced by safety, leaving only progress obligations to be established.

Under the assumption $\square(A \Rightarrow G)$, correctness reduces to proving $\diamond A$. This shifts the burden of reasoning: instead of proving that a correct result is eventually produced ($\diamond G$), it suffices to ensure that some result is eventually produced.

This perspective aligns with several established practices:

• Structured programming: invariants ensure correctness locally, reducing global reasoning to termination
• Contracts and assertions: correctness is enforced at component boundaries, leaving composition to focus on execution
• Concurrent systems: separating invariants from progress conditions isolates correctness from scheduling concerns

In such systems, correctness becomes a structural property, while liveness is reduced to a pure progress concern.

Compositional correctness

Safety properties are well known to compose: invariants established locally can be combined to ensure global safety.

In contrast, liveness properties do not generally compose. Since correctness combines safety and liveness, it follows that correctness does not generally compose either. Under the assumption $\square(A \Rightarrow G)$, correctness reduces to progress: proving $\diamond G$ reduces to proving $\diamond A$. Therefore, when progress composes under suitable conditions, correctness can be established compositionally under the same conditions.

However, for certain classes of programs (e.g., without cyclic dependencies and under fairness assumptions) progress properties can be shown to compose. This yields compositional correctness under the same conditions.

More concretely, in systems composed of multiple parts where progress properties can be shown to compose, correctness can be established compositionally if:

• each part is partially correct (safety);
• each part makes progress when scheduled and executed (local termination);
• a component capable of producing the final observable answer is eventually scheduled.

In such cases, global correctness follows from local safety and compositional progress. This highlights that the difficulty of compositional correctness lies not in safety—which is typically local—but in ensuring that progress composes under the system’s execution model.

In practice, mechanisms such as structured concurrency and the absence of cyclic dependencies help ensure that progress composes by preventing deadlocks and cyclic dependencies.

Example for compositional correctness

Consider a program in which a work queue is introduced to serialize the execution of a set of work items. The question is whether we can reason about the correctness of the resulting program without re-proving correctness monolithically.

Using the design principle outlined in this paper, correctness can be established from local safety guarantees together with structural conditions ensuring progress.

The work queue relies on the following assumptions:

• all work items satisfy the safety properties of the program;
• safety properties are independent of execution order;
• each work item, when executed, eventually completes;
• at least one work item is capable of producing the final observable answer;
• such a work item is eventually executed.

Under these assumptions, a correctly implemented work queue ensures that:

• the safety properties of the program are preserved during execution;
• all work items are eventually executed.

The first property establishes $\square(A \Rightarrow G)$. The second, together with the existence of a work item that produces the final observable answer, establishes $\diamond A$.

By the results of this paper, these two properties suffice to conclude $\diamond G$. Thus, the correctness of the entire program can be established without re-proving correctness monolithically, with the global reasoning isolated to progress assumptions.

Scope and limitations

The reduction from eventual correctness to progress depends on the safety assumption being strong enough: every produced final answer must be correct. If the system can produce intermediate, speculative, partial, stale, or externally observable invalid results, then $\square(A \Rightarrow G)$ does not hold for the relevant notion of answer, and the reduction no longer applies.

Similarly, the compositionality claim is conditional. Safety may compose through local invariants and contracts, but progress composes only under additional structural assumptions such as fairness, absence of cyclic dependencies, bounded resources, or structured lifetimes. The principle does not remove these obligations; it isolates them.

This is the main practical value of the formulation: it does not make correctness automatic, but it makes clear where the remaining proof burden lies.

Conclusion

We have formalised a simple but useful observation:

Under suitable safety guarantees, liveness reduces to a pure progress property.

When all produced outcomes are correct by construction (i.e., $\square(A \Rightarrow G)$), the obligation to prove eventual correctness ($\diamond G$) reduces to proving progress ($\diamond A$). In this setting, correctness no longer depends on which outcome is produced, but only on whether an outcome is eventually produced.

This yields a separation of concerns in correctness reasoning: safety enforces correctness of outcomes, while liveness reduces to a progress property concerned solely with their eventual realisation.

An important consequence is a refined view on compositionality. Since liveness does not generally compose, correctness does not compose in general either. However, under the same safety guarantees, correctness can be established compositionally in systems where progress composes under suitable structural conditions.

Structuring programs so that progress composes yields correctness that composes under the same conditions (provided that safety properties are upheld).

Making this principle explicit clarifies the structure of correctness proofs and provides a simple lens for reasoning about programs, particularly in concurrent and component-based systems.

Keep truthing!

References

• R. W. Floyd, Assigning Meanings to Programs, 1967
• C. A. R. Hoare, An Axiomatic Basis for Computer Programming, 1969
• A. Pnueli, The Temporal Logic of Programs, 1977
• L. Lamport, Proving the Correctness of Multiprocess Programs, 1977
• B. Alpern, F. B. Schneider, Defining Liveness, 1985