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.
