Correctness is hard to reason about as a property of a whole program. Lucian Radu Teodorescu shows how safety and progress can break the problem into composable parts.
In recent years, safety has become a central theme in the C++ community. This has been driven in part by a series of reports from 2022 and 2023 [NSA22, CR23, WH23, EC22, CISA23a, CISA23b] that strongly criticised memory-unsafe languages. The term safety now appears in proposals, talks, and design guidelines, often carrying significant weight (one can find in [McDougall24, Müller25, Doumler25, Bauman26, Vandevoorde26] a small selection of papers that were seen by the C++ standard committee on the subject).
But what do we actually mean by safety?
Given the amount of discussion this topic has generated, one might expect us to have a clear understanding of safety. In practice, this is not the case. The term is often used with implicit and differing meanings. Sometimes it refers specifically to memory safety. Sometimes it refers to the absence of undefined behaviour. Sometimes it gestures towards broader claims about program correctness, security, reliability, or risk. Instead of clarifying a proposal, an argument, or a design choice, the word itself can become the object of the discussion. This is a sign that we lack a shared model, not merely a shared vocabulary.
This article is an attempt to build such a model. We examine the relationship between safety and correctness, using Lamport’s framework [Lamport77] as the starting point. In that framework, safety is not a vague assurance that a program is good, nor a synonym for the absence of memory errors. It is a class of correctness properties: properties whose violation is already visible after a finite part of an execution.
This perspective is broad enough to cover many discussions that currently take place under the name safety: memory safety, arithmetic safety, functional safety, thread safety, and partial correctness. These are not separate meanings of safety. They are different kinds of requirements whose violations are safety violations. The requirements differ, but the shape of the reasoning is the same.
The next step is to connect this model to compositional reasoning. Correctness is difficult to reason about when treated as a single obligation of the whole program. Lamport’s distinction gives us a way to separate that obligation. If safety captures the correctness of any produced result, then the remaining liveness obligation becomes progress: does the program eventually produce such a result? This shift does not make correctness easy, but it gives us a more tractable way to reason about it. Correctness can be decomposed into safety obligations and progress obligations, and programs can be structured so that both are easier to reason about locally.
More broadly, the goal is to better understand the theory behind safety and correctness, and to use that understanding as a basis for writing reasonable code and building correct programs.
Safety and correctness
Prerequisites: requirements
Before we can discuss the safety or correctness of a program, we need to know what is expected of that program. In software engineering, we typically call these expectations requirements. Thus, any discussion of safety and correctness is necessarily relative to some set of requirements.
Some requirements are explicit: a sorting algorithm should return a sorted permutation of its input; a request handler should normally complete within a given latency budget; a component may be required never to perform invalid memory operations. Other requirements are implicit: the program should not halt unexpectedly, execute arbitrary commands, or expose private data to malicious users.
For the rest of the article, we assume that there is a finite list of requirements, explicit or implicit, and that this list is the source of truth when discussing the correctness of the program. In composed systems, these requirements may need to be translated into different local obligations for different program parts.
Lamport’s safety and liveness
A correct program is a program that fully meets its requirements, whether explicit or implicit. Reasoning about correctness directly is hard. To make it easier, Lamport proposes focusing on two different kinds of properties: safety properties and liveness properties [Lamport77]. We follow his definitions:
To prove the correctness of a program, one must prove two essentially different types of properties about it, which we call safety and liveness properties. A safety property is one which states that something will not happen. For example, the partial correctness of a single process program is a safety property. It states that if the program is started with the correct input, then it cannot stop if it does not produce the correct output. A liveness property is one which states that something must happen. An example of a liveness property is the statement that a program will terminate if its input is correct.
The first important consequence is that safety is part of correctness. Safety is not opposed to correctness, and it is not a weaker substitute for correctness. It is one class of correctness properties.
The second consequence is that partial correctness is a safety property. Partial correctness says that, if a program produces an answer, that answer is correct. It does not say that the program eventually produces an answer. That missing part is termination, or more generally progress. Thus:
Total correctness = Partial correctness + Termination
At first, this may seem to clash with the statement that safety properties say that something bad does not happen. But partial correctness can be read negatively: wrong answers are not produced, and this follows the way we defined safety.
This also shows why the wording of a property is not enough to classify it. A safety property may be written in positive or negative terms. For a property P, we can often move between ‘P must not happen’ and ‘whenever we observe an answer, ¬P holds’.
The better test is not grammatical, but semantic: If a safety property is violated, it is violated after a finite prefix of the execution. In simple terms, safety means that no behavioural invariants are violated.
Once a wrong answer has been produced, an invalid memory access has happened, or private data has been exposed, no future continuation can repair that execution. The violation is already present.
Liveness is different: No finite prefix can prove violation of a liveness property.
No matter how long the program has failed to produce an answer, the execution may still be extended with an answer later. Liveness violations are therefore not conclusively detectable in finite time.
One safety to rule them all
Often, when we talk about safety, we need to qualify what kind of safety we mean. Is it memory safety, thread safety, arithmetic safety, type safety, or partial correctness? In the C++ standards committee, there is now a tendency to demand such qualification whenever somebody uses the term safety. For practical purposes, this is a good thing.
However, we should not mistake these qualifications for separate definitions of safety. That would fragment the reasoning about correctness into many seemingly unrelated topics. The important distinction is not between different meanings of safety, but between different requirements whose violations count as safety violations.
If we reflect on the different kinds of safety, we realise that we do not have multiple definitions of safety. We have the same definition, but the relevant requirements vary. Different kinds of safety are given by different kinds of properties, not by different definitions of safety.
The requirements we need for what we call memory safety are different from the ones we need for arithmetic safety, and so on. These names remain useful, but they describe classes of safety properties, not different concepts of safety.
Having one notion of safety allows us to think holistically about correctness. It also lets us look for common patterns across different domains. We can still solve memory-safety, arithmetic-safety, or thread-safety problems separately, but the correctness of the program depends on all of them. It takes only one safety-property violation for the program to stop being correct. There is only one safety, one safety to rule them all.
Undefined behaviour and safety
If a program reaches undefined behaviour, the C++ abstract machine no longer constrains what happens next. The implementation is no longer required to preserve the behaviour encoded in the source code. The practical consequence is that, after undefined behaviour is reached, source-level reasoning no longer applies: anything can happen.
Once undefined behaviour is reachable, we can no longer rely on the source code to preserve any safety property P. Any proof that P holds depends on the execution staying within the rules of the C++ abstract machine.
For this reason, the absence of undefined behaviour is a minimal safety requirement. Other safety requirements can be guaranteed only for executions that remain within the rules of the C++ abstract machine.
Violations of memory safety properties typically lead to undefined behaviour. Thus, it is common to also place memory-safety requirements in the set of minimal safety requirements.
Safe languages
A safe language is not a language in which every program is partially correct. Rather, it is a language that guarantees certain classes of safety properties for programs written within a well-defined subset of the language. For example, a memory-safe language prevents certain invalid memory operations by construction: dangling references, out-of-bounds accesses, or use-after-free errors are either rejected, dynamically checked, or made unrepresentable.
In Lamport’s terminology, this means that the language enforces some safety properties. It does not enforce all safety properties. A memory-safe program may still compute the wrong answer, violate a protocol, expose private data, or execute arbitrary commands. Language safety therefore reduces part of the proof burden, but it does not replace correctness reasoning.
Functional safety
Functional safety is a related concept from systems engineering. ISO 26262:2018 [ISO26262], for example, defines safety as the “absence of unreasonable risk”, where risk is determined from the probability of harm and the severity of that harm. The important point is that functional safety is not about eliminating all risk, but about ruling out risks judged to be unreasonable in a given context. More details can be found in Andreas Weis’s ‘C++Now’ presentation [Weis23].
At first glance, functional safety has little to do with Lamport’s safety. Looking more closely, the two are compatible. In Lamport’s terms, functional safety can be expressed as a set of safety requirements: certain unacceptable-risk states must not be reached. If such a state is reached, the violation is present after a finite prefix of the execution.
The presence of risk factors and probabilities does not change the shape of the property. They help determine which states are unacceptable. Once those requirements are fixed, functional safety fits naturally into Lamport’s safety framework.
Composability
Composability of safety
We often hear that ‘safety composes’. This is true, but the statement hides an important distinction: some safety properties compose almost directly, while others require a non-trivial mapping between local and global requirements.
Let us consider memory-safety properties as a first example. If we have two program parts, A and B, that are evaluated independently, and we find that they uphold all memory-safety properties, then if we put A and B together in a way that preserves their assumptions, we obtain a system that upholds those memory-safety properties. In many cases, the proof is relatively direct.
Now let us look at partial correctness as a safety property. If both A and B are partially correct, it does not follow immediately that the system obtained by putting them together is also partially correct. Composability does not work for partial correctness in the same direct way that it does for memory-safety properties.
The difference is not that memory safety composes while partial correctness does not. The difference is the proof burden. In Lamport’s sense, safety is about preserving behavioural invariants. If A preserves the invariants required of it, and B preserves the invariants required of it, then the composition is safe only if those local invariants are compatible with the requirements of the whole system.
This is where requirements mapping enters the picture. The requirements on A are not necessarily the same as the requirements on B, and neither set is necessarily identical to the requirements of the whole program. To compose partial correctness, we must distribute the requirements of the system to its parts, possibly in different forms, and then show that the local invariants, together with any boundary invariants between A and B, imply the global requirement.
Safety composes. But the proof may require mapping the requirements of the whole system to the invariants preserved by its parts. This is where most of the work is.
A pivot on the meaning of liveness
Safety is local, structural, and compositional. We can build small systems, prove partial correctness in isolation, and then build more complex systems out of them. Liveness is different: it is global, behavioural, and often scheduler-dependent. Reasoning about liveness is harder, and gets harder as the system becomes more complex.
The difficulty is that liveness often seems to carry two obligations at once. We want the program to eventually produce an answer, and we want that answer to be correct. But these are not the same obligation.
This is the pivot: safety can separate the two. Instead of treating liveness in isolation and proving, for every property P, that it eventually holds, we can first prove partial correctness: if an answer is produced, it satisfies P. Only after that do we ask whether an answer is eventually produced. Partial correctness is safety, and safety composes. This means that we can reason bottom-up about whether P is true when we have an answer.
After the safety-related reasoning is done, we can turn our attention to liveness. But the liveness obligation has changed shape. The important point is not that liveness becomes easy, but that its role changes. We no longer need liveness to prove that the eventual answer is correct; safety already gives us that. The remaining obligation is simpler: termination, or more generally progress.
Proving termination or progress is still a global endeavour. But the scope is now reduced, as we have moved much of the complexity towards safety.
For an arbitrary program, we cannot say that liveness composes. But after safety has done the correctness work, the remaining liveness obligation is progress. This is a narrower obligation than full liveness, because it no longer has to establish the correctness of the produced result. We call this safety-refined liveness: liveness after partial correctness has already been established.
If progress composes, so does safety-refined liveness. Thus correctness also composes.
The key is to design programs so that progress composes.
Achieving composable correctness
We can now make the previous pivot concrete. If safety gives us partial correctness, then the remaining question is whether progress can also be made compositional.
In a concurrent program that uses mutexes as the main synchronisation primitive, progress does not compose by default. We can easily get deadlocks and livelocks 1. Progress does not compose automatically.
By contrast, if we use task queues, also known as serializers, and we satisfy a few conditions, progress can be made compositional. A task queue still serialises access to some state, but it does so without requiring work items to block while holding that access.
For example, consider a program structured as a finite chain of work items: one work item parses an input, another validates the parsed representation, and another produces the final output. Each work item may enqueue the next one. If each work item is partially correct, if each work item terminates once scheduled, and if the queue eventually executes queued work, then the whole chain eventually produces a correct result.
Let us separate the assumptions we need.
- For safety:
- work items shall be partially correct, regardless of the execution order;
- the execution order of the work items shall not affect their safety properties;
- For progress:
- each work item makes progress when it is scheduled and executed (local termination);
- at least one work item, or a finite chain of work items, produces the final answer;
- the task queue is fair enough to eventually execute each queued work item.
If the safety assumptions are met, the task queue preserves partial correctness throughout its execution. Partial correctness composes, so we can reason about the partial correctness of the program composed of work items and work queues.
Let us look at progress guarantees. The task queue can ensure that, given a finite set of queued work items, each item will eventually be executed, assuming the queue is fair and each work item terminates. If one of those items, or a finite chain of items, produces the final answer, then the queued system produces the final answer.
Stepping back, we have just argued that progress composes for task queues under certain conditions. If the program is built from components with similar progress guarantees, then progress composes in the same way.
If a program consists only of parts for which progress composes, then the remaining liveness obligation composes. Since safety has already given us partial correctness, correctness composes under these conditions.
This gives us a design principle: Structure programs around components for which progress composes.
Key takeaways
Safety and liveness are not alternatives to correctness. They are ways of structuring correctness properties.
Safety is the absence of broken invariants. Once a wrong answer has been produced, undefined behaviour has been reached, or private data has been exposed (to give a few examples), the execution is already invalid. By looking at invariants, we can say that safety is local, structural, and compositional. Partial correctness is one important safety property: it rules out wrong answers.
Liveness properties state that something eventually happens. The important word is “eventually”. In general, they are harder to reason about compositionally, because no finite execution is enough to show that the required event will never occur.
The useful move is to separate the two obligations. First, use safety to establish partial correctness: if an answer is produced, it is the right kind of answer. Then the remaining liveness obligation is reduced to progress: whether an answer is eventually produced.
This gives us a practical model:
Correctness = safety + progress, when safety has already captured the correctness obligations of the produced result.
The model does not make correctness trivial. Requirements still need to be identified, mapped to program parts, and preserved across boundaries. But correctness need not be treated as an all-or-nothing property of the whole program. Programs can be structured so that local reasoning is easier, progress obligations are explicit, and the path towards correctness becomes shorter.
This leads to the design principle stated above: structure programs around components for which progress composes. More generally, structure programs so that the reasoning effort is pushed towards local, explicit, and composable obligations.
Closing notes
The original motivation for this article was C++ contracts. But before asking what contracts can guarantee, we need a model of what such guarantees are guarantees of. That is what this article has focused on.
We started from Lamport’s taxonomy, which divides correctness properties into safety and liveness properties, and used it to examine safety, correctness, and composability. The main point is that correctness need not be treated as a single all-or-nothing obligation. If safety captures the correctness of any produced result, then the remaining liveness obligation becomes progress. Under the right conditions, both can be reasoned about compositionally.
This does not make correctness easy. Requirements still need to be identified, mapped to program parts, and preserved across boundaries. But it does make the reasoning more tractable: correctness is not a wall that must be climbed all at once, but a path that can be broken into smaller, checkable steps.
In a follow-up article, we turn to contracts. Contracts, whether as a C++ language feature or as a discipline for documenting code, are a natural continuation of this discussion: they make some of the obligations of a program explicit, and therefore easier to reason about.
References
[Bauman26] Jon Bauman, Timur Doumler, Nevin Liber, Ryan McDougall, Pablo Halpern, Jeff Garland, Jonathan Müller, ‘P3874R1: Should C++ be a memory-safe language?’ 2026, https://wg21.link/P3874R1
[CISA23a] Cybersecurity and Infrastructure Security Agency, ‘Shifting the Balance of Cybersecurity Risk: Principles and Approaches for Security-by-Design and -Default’, Apr 2023, https://www.cisa.gov/sites/default/files/2023-04/principles_approaches_for_security-by-design-default_508_0.pdf
[CISA23b] Cybersecurity and Infrastructure Security Agency, ‘Secure by Design’, Apr 2023, https://www.cisa.gov/securebydesign
[CR23] Yael Grauer (Consumer Reports), ‘Future of Memory Safety: Challenges and Recommendations’, Jan 2023, https://advocacy.consumerreports.org/wp-content/uploads/2023/01/Memory-Safety-Convening-Report.pdf
[Doumler25] Timur Doumler, Gašper Ažman, Joshua Berne, P3500R1: Are Contracts “safe”?, 2025, https://wg21.link/P3500R1
[EC22] European Commission, ‘Proposal for a REGULATION OF THE EUROPEAN PARLIAMENT AND OF THE COUNCIL on horizontal cybersecurity requirements for products with digital elements and amending Regulation (EU) 2019/1020’, Document 52022PC0454, Sep 2022, https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=CELEX%3A52022PC0454&qid=1703762955224
[ISO26262] ISO, ISO 26262:2018 Road vehicles – Functional safety, 2018, available from https://www.iso.org/standard/68383.html
[Lamport77] Leslie Lamport, ‘Proving the Correctness of Multiprocess Programs’, IEEE Transactions on Software Engineering 2, 1977, https://lamport.azurewebsites.net/pubs/proving.pdf
[McDougall24] Ryan McDougall, ‘P3578R1: What is “Safety”?’, 2024, https://wg21.link/P3578R1
[Müller25] Jonathan Müller, ‘P3649R0: A principled approach to safety profiles’, 2025, https://wg21.link/P3649R0
[NSA22] National Security Agency, ‘Software Memory Safety’, Nov 2022, https://media.defense.gov/2022/Nov/10/2003112742/-1/-1/0/CSI_SOFTWARE_MEMORY_SAFETY.PDF
[Vandevoorde26], David Vandevoorde, Jeff Garland, Paul E. McKenney, Roger Orr, Bjarne Stroustrup, Michael Wong, ,P3970R0: Profiles and Safety: a call to action,, 2026, https://wg21.link/P3970R0
[Weis23] Andreas Weis, ‘Safety-First: Understanding How To Develop Safety-critical Software’, C++Now, May 2023, https://www.youtube.com/watch?v=mUFRDsgjBrE
[WH23] White House, National Cybersecurity Strategy, Mar 2023, https://bidenwhitehouse.archives.gov/wp-content/uploads/2023/03/National-Cybersecurity-Strategy-2023.pdf
Footnote
- Deadlocks are usually considered safety violations because they can be detected from the current execution state: the program has reached a state in which progress is no longer possible. Livelocks, on the other hand, are liveness violations: the program keeps executing, and no finite prefix is enough to prove that progress will never be made.
has a PhD in programming languages and is a Staff Engineer at Garmin. He likes challenges; and understanding the essence of things (if there is one) constitutes the biggest challenge of all.
