On Contracts and Safety

If two operations are safe, is their composition safe too? At first glance, the answer ought to be yes. But a small expression such as f(g(10)) can appear to contradict that intuition: both functions may be safe under their own contracts, while the nested call still violates memory safety. The missing piece is the caller. Safety does not compose merely because expressions are nested; it composes when obligations and guarantees line up at each boundary.

Building on the previous article [Teodorescu26], this article looks at how contracts help us build safe programs. Contracts give us a structured way to describe obligations and guarantees, both at software boundaries and inside implementations. In that context, we briefly describe C++26 contracts.

We then look more closely at a common source of confusion around the composability of safety. We also consider enforced safe operations as a practical way to build safe programs with respect to selected safety properties. Finally, we look at documentation contracts as a complementary way to express contracts that do not belong in code. Both forms help build safety into applications.

Contracts

‘Design by Contract’ is the discipline of making the obligations and guarantees of software components explicit [Meyer91]. A routine may impose preconditions on its callers, promise postconditions on return, and preserve invariants associated with the object or module it belongs to. The main point is not just that these predicates may be checked, but that they make the boundary between client and implementation explicit.

C++26 contracts bring part of this discipline into the language [P2900]. The core idea is that users can add contract assertions to programs, providing machine-checkable statements about expected program behaviour. These contract assertions come in three forms: preconditions, postconditions, and general-purpose assertion statements.

Listing 1 provides an example of a small function with preconditions and a postcondition. This example is intentionally small. The preconditions, introduced by pre, express what the caller must provide. The postcondition, signalled by post, expresses the guarantees provided by the function on success.

// Changes the name of the user at 'index' to 
// 'new_name' and returns the old name.
std::string update_name(std::size_t index, 
                        std::string new_name)
  pre(index < users_.size())
  pre(!new_name.empty())    // business rule: 
                            // no empty names
  post(r: !r.empty())       // old name must have
                            // been valid
{
  auto& user = users_[index];
  contract_assert(user.is_valid());
  std::string old = std::move(user.name);
  user.name = std::move(new_name);
  return old;
}

Because pre and post appear on the function declaration, they are visible both to callers and to the function implementation. This makes them good candidates for expressing boundary invariants. The contract_assert inside the body checks an internal assumption while implementing that boundary contract. In this sense, contract_assert is a better form of assert, while pre and post are the language features that put part of the contract on the function declaration.

Unlike with the assert macro, the expression given to a contract assertion is always checked syntactically and semantically. We also have better controls for turning contract assertions on and off, and for controlling what happens if the predicate evaluates to false.

Whether a contract assertion is checked, ignored, or enforced is controlled by its evaluation semantic. The available semantics are ignore (do not evaluate the contract assertion), observe (evaluate the assertion, report a violation on failure, and continue), enforce (evaluate the assertion, report a violation on failure, and stop further execution), and quick-enforce (similar to enforce, but allowed to terminate immediately, without attempting to report the violation).

The selected evaluation semantic is implementation-defined and is typically configured through compiler flags.

The application can configure a violation handler that is called when an assertion fails in an observe or enforce evaluation mode. This can be used to perform custom logging or safely shut down critical modules. These options give contracts enough configurability for many real-world applications.

If the function in Listing 1 is called, for example, with an empty new_name, and the evaluation mode is configured to enforce, then the application will terminate, reporting a precondition violation. Similarly, in that same mode, if the function returns an empty name, the application will terminate with an error.

For a short introduction to C++26 contracts, see Timur Doumler’s overview [Doumler24].

Why C++ contracts?

While there may be multiple reasons to use contracts in a codebase, three of them stand out:

• improve reasoning about correctness by replacing implicit assumptions with explicit guarantees;
• allow run-time checking of some invariants, providing empirical validation of the conceptual model;
• improve safety and, as a consequence, improve correctness.

The first benefit is about reasoning at abstraction boundaries. Documentation can express similar obligations and guarantees, but contracts add explicit, machine-checkable structure at the declaration site. When preconditions and postconditions appear in the declaration, both caller and implementer can reason locally: the caller knows what must hold before the call, and the implementer knows what may be assumed inside the routine. This reduces the need to inspect distant call paths and improves modularity with respect to correctness.

The second benefit is empirical validation. Some invariants are hard to verify purely by inspection, especially in large systems, but contracts let us check at run time whether our assumptions hold in real executions. In that sense, contracts do not replace reasoning; they support it with evidence. They help detect mismatches between intended behaviour and observed behaviour, which is valuable both during development and in production configurations that enable checking.

The third benefit is safety, with correctness as a consequence. If more relevant invariants are enforced, fewer invalid states can propagate through the program, and fewer operations execute under violated assumptions. Going back to Lamport’s framing, this improves safety, and because safety is part of correctness, it also improves correctness.

If we considered only the last two benefits, we might be tempted to move invariant checks into function bodies as ordinary assertions. That would still improve empirical validation and safety, and therefore correctness. However, it would weaken modular reasoning about correctness: the caller could no longer rely on an explicit contract at the declaration site, because key assumptions and guarantees would be buried in the implementation. Local reasoning would become significantly harder.

Compositional safety

How safety composes

In the previous article [Teodorescu26] we argued that safety always composes if requirements are properly assigned and distributed to implementation units. However, we did not get into enough detail to clarify why this is true for some common examples.

Let us consider the code in Listing 2. For this example, we intentionally wrote the preconditions as documentation. If the preconditions are upheld, f is memory safe: it does not lead to invalid memory accesses. g is always memory safe. However, the nested call f(g(10)) at the bottom of the listing leads to a memory violation; we attempt to access v[-10].

std::vector<int> v = {1, 2, 3, 4, 5};

// Requires: x >= 0
// Requires: !v.empty()
int f(int x) {
  auto n = std::min(x, (int) v.size()-1);
  return v[n];
}

int g(int x) {
  return -x;
}
...
int r = f(g(10));
...

How come? We said that the two functions f and g are memory safe and we also said that safety composes, and yet a simple function composition gives us a memory violation.

The short answer is that f(g(10)) is not a valid composition of the contracts we wrote down. Function f() is memory safe only under its preconditions. Calling it with a negative argument is outside the domain in which that safety claim applies. The useful question is therefore not whether two arbitrary calls can be nested syntactically, but whether the caller establishes the preconditions required at each call boundary.

To provide an answer to this dilemma, let us start by looking at the functions in our example. How many functions do we have there? If your answer is just two, you are missing one important function: the caller. The code f(g(10)) needs to be placed in some other function; let us call this caller(). We argued that f() and g() are memory safe, but we have not analysed this third function.

The caller has two operations related to our code. The first one calls g(10); the second one calls f() with the result. Now, if we look again at Lamport’s paper [Lamport77], safety is about ensuring that all invariants hold, and these invariants are placed between any two adjacent operations. For this call sequence, the relevant invariant is that the value passed to f() must be non-negative. This is shown in Listing 3.

void caller() {
  auto r1 = g(10);
  // contract_assert(r1 >= 0)
  int r = f(r1);
  ...
}

Indeed, if we look closely, before calling f() the caller must ensure that it does not pass a negative number. The caller has not established that obligation. Thus, while f() and g() are memory safe, caller() is not. The problem is in caller(), not in the way we defined f() and g(). This does not show that safety fails to compose. We were composing two memory-safe operations with one that does not respect the agreed contracts.

Composability unit

The previous example clarifies how composability works. We might assume that in an expression such as f(g(10)) composition happens between f() and g(), but we have shown that this is not the right model. Composability happens through the caller, which establishes obligations and consumes guarantees at each call boundary. This leads to the following realisation:

The composability unit is always caller-callee.

Each time we see apparent sibling composability, such as f(g(10)), we can decompose it into two caller-callee units. In this example, one unit is caller() to g(), and the other is caller() to f() (using the value returned by g()).

This applies whenever we compose functions¹. Expressions like f(g(10)) are syntactic nesting, but semantically they are two caller-mediated contracts in sequence.

Safety and composability flow through obligations and guarantees at each call boundary: caller establishes callee preconditions, then receives callee postconditions. This is where C++ contracts become especially useful: they make boundary contracts explicit and checkable, even when the source syntax is nested.

Exposing clear preconditions and postconditions makes reasoning about correctness at function boundaries easier. It lets us state invariants at the composability unit, empirically validate our model of correctness, and improve both safety and correctness.

If the caller establishes callee preconditions before each call, and each callee guarantees its postconditions on return, then the sequence preserves the safety property.

Enforcing safety

Safe and enforced safe operations

So far, we have looked at safety from the perspective of invariants and composition across call boundaries. That perspective is useful for reasoning about programs as a whole, but it is not always the most convenient way to decide how to build individual operations.

We now turn to a bottom-up perspective: how to build operations that preserve a chosen safety property. Let us start with some definitions.

We define a P-safe operation to be an operation that, when used correctly (all preconditions are met), never violates safety property P. For example, adding two non-negative int values satisfies the property ‘arithmetic overflow cannot happen’ if the precondition a <= INT_MAX - b is met.

We define an enforced P-safe operation to be an operation that never violates safety property P, even if the preconditions are violated. For example, a hardened implementation ² of std::vector may check the precondition of element access and trap when the index is outside the valid range. In such a configuration, the access operation can be treated as enforced memory-safe: an invalid index does not proceed to an out-of-bounds access.

An enforced P-safe operation provides stronger guarantees than a simple P-safe operation. This makes reasoning about safety and correctness easier. Therefore, we should prefer an enforced P-safe operation if there are no significant extra costs attached to it.

The most common way to transform a P-safe operation into an enforced P-safe operation is to check all relevant preconditions and fail early if the preconditions are not upheld. The typical way to fail when preconditions are not met is to trap the program, possibly with a useful message pointing to the violated precondition.

This comes with a caveat. The typical way to build an enforced P-safe operation does not work if P is ‘the program shall not trap’. The only way to ensure that enforcement works for all safety properties P is to refuse to proceed after detecting a precondition violation, turning a safety problem into a liveness problem. This is not a good strategy for most practical purposes, but the caveat is worth mentioning.

So far, we have discussed only enforcing preconditions. While it is possible to use only this strategy to ensure that operations are enforced P-safe, we may want to add checks at different places in our programs. In other words, we may want to check program invariants more often.

Composability

Composing enforced safe operations is much easier than composing simple safe operations. If A and B are enforced safe operations for property P, then calls to these operations cannot violate P, even when the caller fails to establish their ordinary preconditions.

In other words, enforced P-safe operations preserve safety property P, even for sibling compositions. The caller may still violate the operation’s ordinary preconditions, but such violations cannot proceed into a violation of P.

Safe languages such as Rust and Swift improve safety by making many primitive operations enforced safe with respect to selected safety properties. For example, safe Rust prevents memory unsafety in safe code, and Swift checks many operations that would otherwise lead to invalid memory access or undefined behaviour.

There are important qualifications. These languages still have escape hatches: Rust has unsafe, Swift has unsafe pointer APIs, and both languages can interact with foreign code. They also do not enforce every desirable safety property. Instead, they enforce a carefully chosen set of properties at language and library boundaries.

Within the checked subset, however, the composability story is much stronger: if the primitive operations enforce property P, then ordinary compositions of these primitives preserve P without requiring every caller to manually re-establish the low-level preconditions.

C++ contracts, if configured properly, can help turn many operations into enforced safe operations. By trapping on failed preconditions, we can ensure that certain safety properties are enforced in configurations where the relevant contract assertions are checked.

There is a caveat here. In typical C++26 implementations, the person configuring the build can turn off assertion checks. There is no way for a library author to specify that the preconditions should be checked by the compiler in all cases. This means that preconditions cannot be fully guaranteed at the code level.

Even with that limitation, checked preconditions are a significant step up in safety.

Beyond C++ contracts

Contracts are useful, but even if contract assertions are always enabled, they have major limitations:

• not all preconditions, or invariants in general, can be expressed with a contract assertion;
• not all invariants should be checked with contract assertions;
• sometimes, encoding all preconditions and postconditions as contract assertions makes it harder to reason about the code.

For the first limitation, let us imagine a sorting algorithm parameterised by a predicate that dictates the order. The precondition is that the predicate implements a strict weak ordering relation, which is not completely checkable in general. We cannot add contract assertions for invariants whose predicates cannot be expressed in code.

Moving on, some invariants can be checked in code, but are not worth checking, at least not in release builds. Consider the contract of a binary search algorithm. This algorithm has as a precondition that the input sequence is sorted. This is something that we can check. But checking whether the elements are sorted is more expensive than the binary search itself.

Another example is appending an element to a vector, where a good postcondition is to ensure that all original elements remain equal to their previous values and in the same order. To enforce that, however, we need to copy all the elements into a separate storage and then compare them with the resulting vector.

Lastly, expressing contracts in code may make the code harder to read and reason about. Take the sort example again. The preconditions need to include that the input sequence is valid (well-formed and accessible) and that the comparison predicate is a strict weak ordering. The postconditions need to state that the output elements are a permutation of the input elements, and that the resulting sequence is sorted. While in human language it is easy to say “the output is a permutation of the input”, imagine expressing that in code as a postcondition. Assuming all of these are expressible in code, it would still be a lot of code. That extra code needs to be reasoned about, so there is an extra burden. Instead, the contract of the algorithm can often be summarised with a short comment: Sorts the given sequence in place, using the given predicate.

Documentation as contract

Starting from these shortcomings of machine-checkable contracts, Dave Abrahams argues for the idea that documentation is a contract [Parent23]. It is often much easier to express contracts in human language than in a form that machines can understand. Any contract that can be expressed in a machine-checkable way can also be described in human language. When the documentation starts to become too complex, that is a sign that the API may be too complex and may require a redesign.

One counterargument to this viewpoint is that documentation tends to get out of sync with the code. First, this tends to happen more often if the documentation is too large. Large documentation implies a large contract, which implies that the API is too complex. Again, this may be a sign that the API needs to be improved.

Second, we need to analyse this in a broader context to see whether this is really the fault of documentation. When writing a function, we might have contracts at multiple levels:

• an undocumented idea of what the function is required to do;
• what is written in the documentation;
• what is expressed as contracts in the language, for example using C++26 contracts;
• what the tests tell us that the function needs to do, directly or indirectly;
• what the function actually does.

Over time, the contracts expressed at any of these levels can drift away. But there is not always a clear preference for which one is the right contract. Each time we observe a drift, we have a problem that needs to be fixed.

When someone uses the function, they will hopefully read the documentation first. If the documentation is wrong, the function will be used in ways it was not intended to support. At that point, the documented contract and the de facto contract have diverged, and the implementation may be wrong relative to how the API is actually used.

Incorrect documentation can produce unmanaged technical debt at a much higher rate than an incorrect implementation.

Let us look at a very simple, yet powerful example. Listing 4 shows a push_back function for a vector-like class with compact documentation.

// Adds 'e' to the end.
void push_back(E e);

Listing 5 expands part of the same contract into more explicit documentation clauses. If we attempted to express all of those clauses as checked contract assertions, the result would be much more complex, and often much less efficient.

// Adds 'e' to the end.
//
// - Invariant: '*this' is in a valid state
// - Postcondition: 'this->size() == old.size() 
//   + 1'
// - Postcondition: 'std::equal(old.begin(), 
//   old.end(), this->begin())'
// - Postcondition: the last element is equal to 
//   the value of 'e' on entry
void push_back(E e);

The point is not that Listing 4 spells out every detail mechanically. The point is that a clear human-language contract can often carry the intended meaning better than a long list of formal clauses. In ordinary API documentation, “adds e to the end” already tells the reader the essential postcondition: the collection has one more element, the previous elements are still there in their previous order, and the new last element corresponds to e.

After following Dave’s advice for a while, I can report that writing documentation as contracts is one of the best ways to write better code. Having language-checked assertions helps, but it cannot replace good documentation.

Local reasoning

Local reasoning [Parent24] refers to the ability to analyse and verify a defined unit of code, such as a function or class, in isolation, without needing to understand all the contexts in which it is used, or all the details of the code it depends on. These units must have well-defined APIs that separate client-side usage, such as calling a function or instantiating a class, from implementation-side logic, such as the internal details of the function or class.

Local reasoning improves reasoning about programs. Our experience so far suggests that this is one of the hardest parts of software engineering. The complexity of software keeps growing, while human cognitive capacity is limited ³. Local reasoning ensures that the amount of reasoning we need to perform is closer to linear in the size of the program, because we do not have to reason about the same unit of code multiple times in multiple contexts. Local reasoning offers good composability guarantees.

In that sense, local reasoning is one of the central goals of programming.

Contracts are one of the key requirements for local reasoning. If f calls g, then reasoning about f should not require inspecting the implementation of g. Thus, we need the contract of g when we reason about f.

Not having good contracts implies that local reasoning becomes impossible, which complicates reasoning about the codebase. After a certain threshold, reasoning becomes so hard that it tends to invite the accumulation of unmanaged technical debt.

In this context, both code contracts and documentation contracts are useful. Documentation contracts tend to be more concise and easier to read and reason with, but code contracts benefit from empirical verification.

When to use C++ contracts

There are multiple perspectives on contracts. Different people may have different needs from the C++ contracts feature. Here, I will briefly set out my current perspective on using it.

Reasoning is still the main goal. C++ contracts help local reasoning by making some obligations and guarantees explicit at program boundaries. The help is limited: documentation contracts may do a better job for contracts that are too complex, too expensive, or impossible to encode as contract assertions.

C++ contracts do not replace contracts written in documentation. We still need good documentation to reason about the code. We should make sure that what we express with C++ contracts matches the human-readable documentation.

C++ contracts may provide empirical evidence that our reasoning is correct. In this sense, we use the language to validate our assumptions.

C++ contracts can help provide enforced P-safe operations, for various properties. This is especially useful for protecting against undefined behaviour.

C++ contracts are essentially a safety feature. Contract checking is about ensuring that invariants hold; in Lamport’s framing, this is a safety concern. The benefits above compound: clearer reasoning, empirical validation, and enforced checks all make it easier to write programs that do not accidentally violate safety properties.

Takeaways

The small f(g(10)) example is a useful reminder. At first glance, it looks as if two safe functions were composed and safety failed. But the missing piece was the caller. Once we look at the caller-callee boundaries, the problem becomes clearer: one of the contracts was not respected.

That is the pattern contracts help us see. They turn hidden assumptions into visible obligations and guarantees. Safety composes when each caller respects the contracts of the operations it uses, and even syntactically nested expressions can be decomposed into these caller-callee units.

Once those boundaries are visible, we can ask a stronger question. Do we merely rely on the caller to satisfy a contract, or do we stop execution when the contract is violated? This is where enforced safe operations become important. The more we use them, the more we increase safety in the application.

C++26 contracts can support this style of programming through local reasoning, empirical validation, and enforced safety, depending on how checking is configured. Still, documentation contracts remain essential. Some contracts are too complex, too expensive, or impossible to express in code, and they still need to be part of the reasoning structure of the program.

In any case, contracts remain one of the best tools we have to improve the safety of our programs.

References

[Doumler24] Timur Doumler, ‘C++ Contracts in 5 Minutes’ on TIMUR.AUDIO, posted 30 January 2025 at https://timur.audio/contracts_explained_in_5_mins.

[Lamport77] Leslie Lamport, ‘Proving the Correctness of Multiprocess Programs’, IEEE Transactions on Software Engineering 2, 1977, https://www.microsoft.com/en-us/research/publication/2016/12/Proving-the-Correctness-of-Multiprocess-Programs.pdf.

[Meyer91] Bertrand Meyer, ‘Design by Contract’, in Advances in Object-Oriented Software Engineering, D. Mandrioli and B. Meyer (eds), Prentice Hall, 1991.

[P2900] Joshua Berne, Timur Doumler, Andrzej Krzemieński, et al., ‘P2900R14: Contracts for C++’, https://wg21.link/P2900R14.

[P3471R4] Konstantin Varlamov, Louis Dionne, ‘P3471R4: Standard library hardening’, https://wg21.link/P3471R4.

[Parent23] Sean Parent and Dave Abrahams, ‘Better Code: Contracts in C++’, CppCon 2023, https://www.youtube.com/watch?v=OWsepDEh5lQ.

[Parent24] Sean Parent, ‘Local Reasoning in C++’, NDC TechTown 2024, https://www.youtube.com/watch?v=bhizxAXQlWc.

[Teodorescu26] Lucian Radu Teodorescu, ‘Safety, Correctness, and the Shape of Reasoning’, Overload 193, June 2026, https://accu.org/journals/overload/34/193/overload193.pdf#page=6.

Footnotes

1. Coroutines are operationally more involved, but they follow the same boundary principle.
2. C++26 introduced a hardened mode in which extra run-time checks are done for common operations in the standard library; the reader can consult [P3471R4] for more details.
3. Local reasoning also seems important in the age of AI, where LLMs are writing more and more code. But that is a larger topic; we will leave it for another article.

Lucian Radu Teodorescu 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.