Data pipelines rarely fail, they usually mislead quietly.

My last post, Towards a data discipline, explained why we need a data discipline. A way of building data systems to prevent errors by design, instead of detecting them after the fact.

This post turns that into a practical step by step recipe. It follows the spirit of Karpathy’s recipe for training neural networks. His observation that badly trained networks rarely announce errors, and just quietly perform worse, is shared across data systems including data pipelines. The main reason for this article is to document a process for building data systems that are correct by construction. This post may be opinionated (read: biased), so any criticism is very welcome.

This is part one of the Towards a Data Discipline series:

The first post explained the main principles.
This post gives a step by step recipe to follow.
And the last part will focus on writing more complex formal arguments.

A worked example:

We will follow a small imaginary data pipeline in the whole article. This pipeline is deliberately simple so that we can focus on the principles.

A service emits two kinds of events: orders or refunds
Each has: id, an amount in euros and the time it happened. Events are delivered at least once, so duplicates can happen, and they can arrive late.

We must produce a table to show to the finance team, daily_revenue, with one row per day containing: gross sales, refunds, net revenue and the number of orders.

The good news about proofs and formal methods

I want to make this clear. Formal methods have a reputation for being complex and expensive. And some of them are. But, in my experience, most errors are caught at the less formal end: when you try to write a falsifiable statement, when you list assumptions, and when you try to explain, in simple words, why a property holds. More complex solvers and proof assistants are for the few properties where a mistake is expensive and the argument is easy to get wrong. The next post will go into more detail on proofs and writing arguments.

The full recipe

We build things in the wrong order today:
write ad hoc code → write tests, maybe → ship and decorate with monitoring.

And we end up introducing a lot of new concepts such as data contracts, SLAs, SLOs, etc. etc. I would argue that skipping explicit reasoning about correctness is a big part of why we keep reinventing ideas that other engineering fields have always been using.

This recipe changes the order in which we do things:

For the sake of repetition: skipping a step is allowed but should be explicit.

#0 - Define as you go

As we mentioned already: you cannot define a data system you don’t understand, and you will not understand it unless you get your hands dirty with some experimentation first.

0.1. Experiment

Open a notebook, look at the events, do some exploratory data analysis, look for inconsistencies, duplicates, patterns, ask a domain expert etc. All of this can give you insights such as: all events “usually” arrive within a day, or that “daily” means a different thing for the finance team than it does for the logistics team etc. etc.

The goal of the experimentation step is not to be restrictive. But it has an exit condition. You are only done with experimentation when you can: state the problem properly, when you have an idea of how you can solve the problem (a rough sketch of a design you think will solve it), and you have a clear set of assumptions (such as what “daily” means etc.)

0.2. Define what correct means

After the experimentation, we may be able to have our definition of “correct” as something like this:

For 3 consecutive weeks,
rows for day D are successfully published by 07:00 UTC on D+1 at least 90% of the time. And by 08:00 UTC at least 99% of the time.
And once day D is closed, from D+4 onwards, its net revenue matches the finance ledger to the cent.

Now, if you want to evaluate your definition, here is a question to use as a test:
“What observation would imply your statement is incorrect?” If there is no observation that will show your statement is incorrect. Then your statement is not falsifiable.

I know that at times this can be hard to do for certain problems, but we have to start somewhere. When you approach a problem without having a proper definition, you are still having an implicit definition, so we must never use “this problem is hard to measure” as an excuse. The choice is between having this definition be implicit or having it explicitly and clearly stated.

As we previously mentioned measurements do mislead. Once a number becomes a target, people tend to optimise the number instead of what is meant. This is one more reason why we have to write down the assumptions.

0.3. Keep a list of assumptions

Write all the assumptions (and simplifications) you gather along the way in a register of assumptions. This can be a markdown file near the documentation.

Every pipeline rests on a set of small beliefs and decisions. Not writing them down will almost always come back to haunt you. Writing them down can be useful for us to decide: do we want to prove this, check for it, monitor it, or accept it if it’s trivial.

Here are examples of assumptions for our finance data pipeline above:

A1. Every event arrives within 24 hours of when it happened. (Observed maximum: 21 hours.)
A2. Every event has a unique id. Events may be delivered more than once, but a duplicate event is identical to the original.
A3. Amounts are positive, in euros, in whole cents.
A4. A “day” is a calendar day in UTC. (Confirmed with Anna from finance on the 17th of September 2025)

What matters here is that these assumptions can be cited later, they can be checked and updated, and they are open for review.

Step #0 can be considered done when: you have a clear statement of what it means for your system to be “correct”. You have a rough sketch of how to solve it and have verified that through experimentation. You have a register of assumptions about the world and what different definitions mean.

Has this been helpful so far? share it with someone you think will benefit

Share

#1 Prove what you can

Because this step needs an article on its own, I will only introduce the simpler ideas here and a more detailed version is available in the next post here.

Now is the time to design and architect the data system. As we do so we will want to define “what properties must be true, and how can we convince someone else that they are?”.

This forces a modular design! Dijkstra puts this more eloquently when he said that the competent programmer is “fully aware of the strictly limited size of his own skull”. A proof of an entire pipeline cannot be reviewed, if at all can be written. A proof of one critical function is usually reviewable and relatively easy to write.

State the properties to prove

The entire goal of this step is that you have a list of properties to prove in a proof register. In this register we want to have:

what we want to prove: properties that the data system should guarantee.
how we want to prove it: we will do this in the next step, more critical properties may require more formal proofs, or other forms of validation.

The definition step before should have given us: 1. A statement about the whole data system. 2. A list of assumptions. 3. A rough design of the system that can be improved upon. The first thing I would do in this case is select from this what parts of the system are more critical in terms of correctness. Before we jump into generic properties like idempotence and determinism, we first want to show the system achieves its specific goals.

In our example, we can take part of the statement: “For 3 consecutive weeks, rows for day D are successfully published by 07:00 UTC on D+1 90% of the time” And see what it implies for each module in our design. What each module needs to verify to achieve this, and which modules are more critical to this statement. For example, the scheduler must start early enough, and the job must finish by 07:00 UTC. Add all those properties to your proof register.

On general properties to validate for data pipelines: After the above (specific) properties are added, in the case of a data pipeline we can add things that come up often. I have found the following list useful to go through, and I’m sure I have missed a few others. The reason they keep turning up is because retries, redeliveries, late data, etc. are usually part of every data pipeline. None of these are surprising to any data engineer, and they cover a big share of what goes wrong:

Determinism: the same inputs give the same output, whatever the order in which they arrive, or how many workers process them.

Idempotence: running the job twice for the same day leaves the table exactly as running it once. This is what makes retrying your job harmless.
Incremental equals full: in other words that running the job every day for a month produces the same table as rebuilding it at the end of the month in one go. Think of when a backfill produces a different result from what you have been publishing daily, and now you have to explain which one is true.
Conservation: nothing is created or lost in transit. In our pipeline example, every received event ends up in exactly one place: either accepted or quarantined. Keeping the raw history immutable makes this easy to verify.
Invariants: what must be true of the output at rest (independent from how the pipeline ran or how it’s designed). For example in our pipeline this can mean: exactly one row per day, or the fact that net revenue equals the gross revenue minus refunds.
Isolation between runs: two overlapping runs must not overwrite each other’s results. A retry still running when the next day’s run starts could cause issues.

I am not arguing that any of these properties must be guaranteed in every data system. These are properties I personally look at from time to time to check if they are needed in a specific scenario. Maxime Beauchemin’s article from 2018 on functional data engineering is still a read I would recommend for reasoning about some of these. Although it focuses on Airflow, much of it is generalisable.

Beyond data pipelines: the same principle applies to any data system: start from what the system is for, and ask what each module must guarantee for that to hold. The following are a few other properties from other kinds of system, each of which I have seen being repeated in enough cases to put as a list:

For training sets used in an ML model: no feature value is used before the moment it would have been known. The absence of point in time correctness will lead to leakage.
A pricing model: all else equal, the predicted price never decreases as floor area grows. XGBoost and LightGBM can guarantee this by construction, through monotonic constraints.
An access layer: no combination of roles can read a column tagged as personal data (AWS for example uses an SMT solver to answer such questions, we will talk more about SMT solvers in the next post).
Schema migration: queries run against the old schema return the same rows against the new schema.

Are there any similar things that you often see repeated? It would be very helpful if you let me know here in a comment.

Decide how hard you will prove each property

A proof can go from: a written argument in the design docs, to a structured argument, such as induction over partitions. Or even a machine-checked model or proof (such as using TLA+ for concurrency and orchestration)

More formal proofs are not always better. They are more expensive, but provide stronger guarantees to prevent errors. There are two questions I would ask to figure out what level to choose: “what does it cost us if this is false?”, and “how easy is it to get the argument wrong?”. I wrote more details on this in the next post.

From all the above we can complete our proof register, this list will now have what we want to prove and how we intend to prove it (including what we will not prove and why). Here’s an example for our daily revenue pipeline:

Proof register:
P1. determinism: type guarantees and a written argument. Depends on assumption A2.
P2. idempotence: written argument. Depends on P1.
P3. daily revenue matches the finance team definition. Type guarantees and a written argument. Depends on A2, A3 and A4.
P4. daily revenue is the same whether the table was built daily or rebuilt once (incremental equals full): a structured argument, by induction. Depends on P1 and P6.
P5. the job is ready by 07:00: statistical argument by running multiple times (on the edge examples) and reporting the distribution of time it takes to run.
P6. no on-time event is missed: if an event satisfies A1, it is accepted before the last run that recomputes the day of that event. Machine-checked, with SMT solver. Depends on A1 and on the scheduler.
P7. isolation: an overlapping retry never overwrites newer results. Validated through an exhaustive check of possible interleavings.
Not proven: agreement with the ledger depends on the finance system.
Not proven: the scheduler runs the job at all, which is someone else’s software. Both go to monitoring.

The last lines matter just as much. A reviewer can now see what we skipped and argue about it.

As a summary, before you leave this step you should have a proof register including:
what you will prove.
how you will prove it.
what you choose NOT to prove should be explicit.
The next article has exact steps to help you decide this with an example.

Write the arguments before writing code

Write the arguments before you write code. Quick falsification (a few tests, a small script) is still worth doing at any step, because it is the cheapest way to find out an argument is wrong, and perhaps you would have done much of this during the experimentation step but it is the argument that usually tells you what to test.

Now we have a list of things to prove and how we will prove each one.

Let’s only look at the simple arguments here, and keep the more complex ones for the next post.

P1. determinism: the function reads nothing about the environment (no clock, no environment variables, no randomness). It removes duplicates by id, which cannot depend on the order of arrival (A2). The order of summation does not matter, since amounts are Decimals, and Decimal addition is exact within the precision we need. The output therefore must depend only on the set of accepted events for that day.

Note that, for example, the last sentence could be false if we had floats in Python, (0.1 + 0.2) + 0.3 gives 0.6000….0000001 and 0.1 + (0.2 + 0.3) gives 0.6. Which means that the total could depend on the order, and produce different numbers for the same events.

P2. idempotence: running on day D replaces partitions from D-3 to D with values computed from the accepted events for those days. Replacing a value with the same value twice is the same as doing it once, and gives the same value.

That argument would fail, if the job appends rows instead of replacing partitions, and the system would fail on a retry. It also assumes P7, that there is no issue with overlapping jobs (we will argue for P7 in part 3).

These examples are perhaps too simple, but think of how many times we actually try to argue for idempotence and determinism when we build data pipelines. Very rarely.

For the more complex end of arguments check the next blog post on formal methods here.

Write the tests and the code

Write the tests for the arguments above. Tests now have a precise job, they do not ask about a few examples you can think of on the fly. They ask whether the code follows the properties you care about the most.

Property-based testing fits well here and the next post will show an example of it, with a library such as Hypothesis in Python. Each test states a property from the register, and Hypothesis generates hundreds of inputs that satisfy the preconditions and tries to break the test. Because they can find counterexamples early, it is justified to use property-based tests before investing time in writing an argument.

For writing good tests I would defer to: the testing section of Software Engineering at Google, How to Specify It! by John Hughes for property-based testing, and Google’s ML Test Score for data and ML systems.

Then you can write the code matching the design, and while doing so write the types and contracts that encode the assumptions, and the functions and jobs that attempt to guarantee them.

Definition of done: you are done with this step when the properties in your register are argued for, every argument names the assumptions it relies on, and every property has a test (or a machine-checked proof).

#2 Check at every boundary

Now is the time where we put those assumptions to a good use.

Check at the boundary: means simply execute the precondition.

In our example, we have four clear boundaries:

We receive raw events from the checkout service that become accepted events.
Those accepted events are handed over. No check is needed here: the types and parsing should already fulfill our needs.
When writing to the table that is handed to the finance team.
The orchestrator’s config, which must run as expected at the time expected.

When the events are received we can make use of the idea of parse don’t validate (recommended read by Alexis King) to parse the events in a way that holds the assumptions. If an event fails we can reject them and add them to a quarantine table instead of correcting them and letting an error leak into the results.

Isolating late events, for example, is not only good practice in this case, our proof for incremental-equals-full, which we will write in the next post, depends on it. Note that for our example, if we reject a late event and put it in quarantine, the results will probably disagree with the finance team’s calculations. But this will help us review our assumptions about late events, and will also be relatively easy to figure out.

When the events are written we need a contract with the reader (in our example the finance team). This should contain for example:

Structure: one row per UTC day, including days without sales, with the columns day, gross, refunds, net and orders.
Meaning: amounts in euros, net equals gross minus refunds, net may be negative.
Delivery: provisional by 07:00 UTC on D+1, and final from D+4, and a final day never changes again without an announced reopening.

Two things about this contract. First, “net may be negative”: writing down what is allowed matters as much as writing down what is not: it is what stops a well-meaning colleague from trying to fix it. Second, “a final day never changes”: it follows from the design (each run only replaces partitions D-3 to D, see P2), since no run touches an older partition. We promise something we have argued for.

In Meyer’s terms, what we did here is: use the parser to state the preconditions, and the contract to state the postconditions to the finance team (and “one row per day” and “net equals gross minus refunds” are invariants that must hold)

Definition of done for step 2: every assumption about the world in the register is checked at the boundary where it enters, or there is a written note explaining why it cannot be; and every promise to downstream users is written down

#3 Monitor the rest

Whether the world keeps behaving the way the register says it does, whether the evidence behind our statistical arguments still applies, and whether the system as a whole meets the statement from step 0. Monitoring is now a short list, because we know exactly what to watch. Every item on it points to what it is for:

A1. events arrive within 24 hours: the quarantine count and the distribution of delays. Any quarantined event alerts the pipeline owner, who reconciles with the source team and decides whether to reopen the day.
P5’s evidence: the job’s runtime against the benchmark. A run still going at 06:45 is an early warning, not yet a breach.
Not proven, the scheduler: if no run has started by 06:15, alert.
Not proven, the ledger: from D+4, a daily reconciliation against the finance ledger. Any difference goes to the pipeline owner and to Anna.
The definition itself: the weekly share of days published by 07:00, against the 90% in step 0, and by 08:00 against 99%.

As stated in the earlier post, every monitoring artefact should have: an owner, a publishing channel, and an action (this clarifies what to do in case of an alert and who does it).

Definition of done: assumptions that cannot be proven or that must be monitored anyway have a monitor, or an explicitly written acceptance of the risk. And every monitor has an owner, a channel and an action.

Optimise

Only now can you parallelise, pre-aggregate, change engines, and all that. But every change must preserve the properties. As Dijkstra wrote (in his essay How do we tell truths that might hurt?) “Simplicity is prerequisite for reliability,” it’s also a prerequisite for optimisation.

Conclusion

Is this too much to ask? This is a real question, not a statement. When I started this series, I worried that some of it may be too much. But look at the simplest version of this: a falsifiable statement, a few assumptions, a few lines of argument, a parser and a contract. That “should” be a few hours of writing, which would prevent days of fixing or worse. The expensive parts (like using a proof by induction, using solvers or statistics) are reserved for the properties that deserve that time.

Now that we use assistance from LLMs to write much of our code, this discipline matters even more. The definitions, the assumptions and arguments are good things to work on without help from any AI assistant. Writing code has become faster, let’s try to keep a certain base level of understanding.

So, honestly, if you are a data or ML engineer, do you think this is too much?

Leave a comment

Next post uses this same pipeline but will focus on the arguments themselves: how hard to argue for each property, with example proofs and using a solver and an exhaustive check.

Subscribe now

Experiments

A Recipe for “correct” data systems