Some of the most serious system flaws can be detected before code is written if the design itself is treated as a system that can be analyzed. This is the focus of Hillel Wayne’s presentation, which explains how principles from formal methods can help examine future systems and uncover resilience, concurrency, and failure issues before they become operational errors.
Wayne begins with a simplified example of what he calls a “task executor”: the system checks whether the task has been completed, marks it as complete, and then performs the task. The sequence seems logical, but it breaks down when a failure occurs during execution. A retry may take place after the task has been recorded as complete, so the task is never actually performed. Moving the completion record to after execution creates another problem: two concurrent executors can perform the same task twice before either one records its completion.
This is not merely a theoretical problem; the presentation connects it to examples such as parcel-delivery systems that may send an order twice, scheduling systems that may book the same appointment for two people, and application-installation mechanisms that may enter destructive behavior when a request is repeated.
Start by Defining What “Correct” Means
Wayne proposes expressing system requirements as binary properties: they are either true or false. Examples include ensuring that a task is not performed more than once, which is a safety property that prevents something bad from happening, and ensuring that the task is performed at least once, which is a liveness property that guarantees something desired will happen.
The presentation emphasizes that properties are not equally strong. A system capable of processing 10,000 queries per second automatically satisfies the property of processing two queries per second, but the reverse is not true. Therefore, passing a strong property may demonstrate the correctness of a set of weaker properties, while failure of a weaker property helps narrow down the cause of a fault. Wayne connects this idea to the testing pyramid: numerous unit tests may be more useful for diagnosing an error than a limited number of end-to-end tests.
The Simplified Model Reveals the Core Problem
Rather than representing the system with all its details, Wayne advocates building an abstract model containing only the minimum necessary state: the current stage of the algorithm, whether the task is marked as complete, and the number of times it has been performed. This makes it possible to explore possible states and the paths the system can take, including failure and retry scenarios.
In formal methods, this model and its properties can be encoded using logical formulas and then checked with tools such as model checkers and SMT solvers. However, the practical idea in the presentation does not require using these tools directly; an engineer can adopt the same way of thinking by tracing possible states and transitions.
The “Adversary” in Concurrency and Failure
Wayne suggests viewing every source of nondeterminism, such as user input, concurrency, randomness, timeouts, and server outages, as an “adversary” that always chooses the worst possible outcome. If the system can retry indefinitely, this adversary will choose failure every time, revealing that the liveness property is not guaranteed even if success is theoretically possible.
He also explains that having concurrent executors requires representing some variables as local to each process and others as shared between the system and the outside world. By exploring different execution orders, it is possible to reach a state in which the task is performed twice, even when each executor appears sound on its own.
Assumptions Are Part of the Design
A system’s correctness depends not only on its properties but also on the assumptions about the environment in which it operates. One design may require the strong assumption that a process never fails, while another may work if failure occurs a limited number of times. Wayne notes that reordering steps may reduce liveness assumptions, but it may increase safety requirements, such as the need to guarantee that only one executor is active at a time.
The situation also changes when the operating environment changes. Relying on strong consistency in a database and then moving to eventual consistency may make properties that were previously true no longer guaranteed, even if the system’s code has not changed. Therefore, assumptions about the service provider or database should not be considered external details; they are direct conditions for the correctness of the design.
What Changes in Practice?
The practical value of this approach is not to replace testing or to call for the use of formal tools in every project, but to make design questions more rigorous: What states are possible? What is the worst ordering of events? What do we actually control? And which assumptions cannot the team guarantee? The stronger the required property or the less predictable the environment, the more complex the system’s design must be, or the required property must be relaxed—for example, changing the condition “process every message” to “process messages or send them to a dead-letter queue.”
Wayne presents these ideas as thinking tools derived from formal methods, not as a ready-made substitute for engineering judgment. The open question in every system remains how accurate the model and the assumptions used are; if a state is omitted or the team assumes behavior that the environment does not guarantee, the analysis may prove the correctness of a model that does not resemble the real system.