Building Barista—Part 2: Formal Verification and TLA+

Nov 12, 2026

☕ Welcome to The Coder Cafe! Part 1 of Building Barista covered the architecture. Today, we explore formal verification through a real bug my tests missed. You’ll learn what model checking is, how to read a bit of TLA+, and why it catches the bugs we never think about. I spent a lot of time on formal verification at Google; this time, I pointed it at my own system. Get cozy, grab a coffee, and let’s begin!

One Email a Day

A quick summary of Barista: it’s a system I built that fetches hundreds of sources, gets a unique prompt per user, and sends that user one email per day with the best sources for them.

Making sure Barista sends a single email per user per day is something important to me. If Alice receives the same email twice on a random day, that’s a terrible user experience.

As discussed in Part 1, Barista is a set of independent stages coordinating through Postgres. The last one, Send, runs every 5 minutes, looks for the users whose send time has passed, and emails each of them the posts picked by the Rank stage.

The nominal scenario:

The Send stage starts and notices an email has to be sent to Alice.
Barista calls the email provider and receives an ACK.
✅ Barista writes back in Postgres that the email to Alice was sent that day.

Now the worst-case scenario:

The Send stage starts and notices an email has to be sent to Alice.
Barista calls the email provider and receives an ACK.
❌ Before writing back in Postgres that the email was sent, Barista crashes.
The Send stage starts again and notices an email has to be sent to Alice.
Barista calls the email provider again and receives an ACK. ← Duplicate email
✅ Barista writes back in Postgres that the email to Alice was sent that day.

How do you prevent that? I picked my email provider for it: Plunk. Why Plunk? Because it accepts an idempotency key.

When calling Plunk, I pass a key like alice-20260520: the user and the day. If Plunk receives the same key again, it doesn’t send anything; it replies with a 409. My code reads that 409 as “these posts were already sent” and marks them as sent. No duplicate.

It was a conscious decision. Plunk is 10x more expensive per email than AWS SES, which has no idempotency key. I was happy to pay for it.

So here was the state:

A business decision: no duplicates, even if it costs more.
A sound design, with an email provider deduplicating for me.
Unit tests, integration tests, end-to-end tests. All green.

Great mental model of the code. Pure intellectual control.

Now, what if I told you my code had a bug? One that none of my tests caught. I only managed to find it with something called formal verification. Let’s see how.

Barista banner from The Coder Cafe. On the left, a small gold “BARISTA” label sits above the headline “Want to give it a try?” and the line “Write your own brief, and your first email lands in seconds.” On the right is a flat illustration of a café counter in tan and brown tones. A sign above it reads “The Coder Cafe”, and pendant lamps hang over a laptop, a coffee cup, an espresso machine and a potted plant, with a white bar stool in front.

Formal Verification

Before becoming an SRE, I worked in Air Traffic Management (I talked about it in Reliability Explained). It’s a so-called safety-critical domain. You can easily imagine why.

In a safety-critical system, green tests aren’t enough. That’s the blind spot of intellectual control: tests only check the scenarios we thought about. And the bugs that hurt are, by definition, the ones we didn’t think about.

In domains like this, green tests aren’t the end of the conversation. Some teams go further and prove that certain bugs can’t happen. Airbus, for example, used a static analyzer called Astrée to prove that the flight control software of the A340 and A380 is free of a whole class of runtime errors.

So instead of picking scenarios one by one, what if we could check all of them? That’s the idea behind formal verification: describe the system precisely, write down the properties it must respect, and let a tool check that no possible execution breaks them.

Note the word: verification. It answers “did we build the thing right?”, meaning does the design respect our properties. Not to be confused with validation: “did we build the right thing?”, meaning are these the properties we actually need. A tool can do the first. The second stays on us.

Model Checking

There are several ways to verify a system, from mathematical proofs to running real code on generated inputs. The one I used is model checking.

A model checker sees a system as states (a value for every variable) and actions (a step from one state to the next). It starts from the initial state, tries every possible action, then every possible action from each new state, and so on, until it has visited every reachable state. A test follows one path. A model checker walks all of them.

That’s why it finds bugs nobody writes a test for. AWS described it in 2015, in a paper on how they use formal methods: one of their DynamoDB bugs had survived design reviews, code reviews, and testing. The shortest sequence of events to trigger it was 35 steps long.

At each state, the model checker checks our properties. They come in two flavors:

Safety: Something bad never happens (e.g., Alice never receives the same email twice)
Liveness: Something good eventually happens (e.g., Alice eventually receives her daily email)

When a property breaks, we get a counterexample: the exact sequence of steps that led there.

TLA+

The model checker I used is TLC. It reads models written in TLA+, a language created by Leslie Lamport to describe a system as states and actions. In other words: we describe the system in TLA+, and TLC explores every state it can reach.

A TLA+ spec doesn’t look like code. There are no instructions executed one after the other. Instead, each action is a formula that says two things: when the step is allowed (a condition on the current state), and what the state looks like after it (the values in the next state). TLC then tries every allowed action, in every possible order.

A few symbols are enough to follow the examples below:

== means “is defined as”
/\ means and
x' is the value of x in the next state
\A and \E mean “for all” and “there exists”

Let’s see it on a simple example. Imagine a cafe with one croissant left and two baristas. When a customer asks for a croissant, a barista does two things: first, they check the display case to see if there’s one left; then, they sell it.

The property we want is a safety one (something bad never happens): the cafe never sells a croissant it doesn’t have. In other words, the stock never goes below zero.

To model this cafe, we need two variables:

stock: how many croissants are left. It starts at 1.
step: where each barista is. Each one starts "idle", moves to "selling" after checking, and ends "done".

Now, the two actions. The first one is checking the display case:

Check(b) ==
    /\ step[b] = "idle"                        \* b hasn't started yet
    /\ stock > 0                               \* and there's a croissant left
    /\ step' = [step EXCEPT ![b] = "selling"]  \* next, b is selling
    /\ UNCHANGED stock                         \* the stock doesn't change yet

The first two lines are conditions: Check can only happen if barista b is idle and there’s a croissant left. The last two lines describe the next state: b is now selling (EXCEPT means “every other barista stays where they are”), and the stock stays the same.

The second action is selling:

Sell(b) ==
    /\ step[b] = "selling"                     \* b has checked the case
    /\ stock' = stock - 1                      \* next, one croissant less
    /\ step' = [step EXCEPT ![b] = "done"]     \* and b is done

And the property, written as an invariant that must hold in every state:

NeverOversold == stock >= 0

That’s the whole model. TLC starts from the initial state (one croissant, two idle baristas) and tries every action, in every possible order. In most orders, everything is fine. For example, barista 1 checks and sells, then barista 2 can’t check anymore because the stock is zero.

But TLC finds one order that breaks the invariant:

1. Initial     stock = 1    b1 idle      b2 idle
2. Check(b1)   stock = 1    b1 selling   b2 idle
3. Check(b2)   stock = 1    b1 selling   b2 selling
4. Sell(b1)    stock = 0    b1 done      b2 selling
5. Sell(b2)    stock = -1   b1 done      b2 done     <- invariant broken

Both baristas looked at the display case before either one sold. Both saw a croissant. Both sold it.

That’s how to read a counterexample: find the step where it broke (5), then walk back to the decision that made it inevitable (3). The fix is to make checking and selling a single action, so nobody can slip in between. Re-run TLC, and it explores every state without finding a violation. In a cafe, we can merge two steps. Across a network call and a database write, we can’t, and that’s exactly why idempotency keys exist.

Now, let’s do the same with Barista.

Verifying Barista

Back to Barista. Years after leaving Air Traffic Management, I wondered: what if I applied the same rigor here? So I wrote a TLA+ spec of the Send stage.

The model was tiny: one user, two posts, a clock with eight slots per day, and two days. The key idea is that it tracks two things separately: what was really delivered to the user, and what Barista believes was delivered. If Barista works, both always agree. The full spec also has a few actions I’m leaving out here: the clock ticks, Rank picks new posts, and Send moves the next send time forward.

Here are the variables (simplified):

now: the clock.
sched[u].send: when user u’s next email is due.
picks[u]: the posts picked for u’s next email.
plunkKeys: the idempotency keys Plunk has already seen.
emails: the list of emails really delivered. The truth.
sent[u]: the posts Barista has marked as sent to u. What Barista believes.

And a simplified version of the Send action at the time:

Send(u) ==
  LET key == <<u, UTCDay(now)>>    \* the key: user + current UTC day
  IN
  /\ sched[u].send <= now          \* u's send time has passed
  /\ IF key \in plunkKeys          \* has Plunk seen this key?
       THEN UNCHANGED emails       \*   yes: 409, nothing is delivered
       ELSE emails' = Append(emails, [to |-> u, posts |-> picks[u]])
                                   \*   no: 200, the email is delivered
  /\ plunkKeys' = plunkKeys \cup {key}
                                   \* Plunk remembers the key
  /\ sent' = [sent EXCEPT ![u] = sent[u] \cup picks[u]]
                                   \* either way, the posts are marked as sent
  /\ ...                           \* scheduling and other variables omitted

A few new pieces: LET … IN defines a local name (here, the key). <<u, UTCDay(now)>> is a pair, our alice-20260520. \cup adds to a set, and Append adds to the end of a list. And [to |-> u, posts |-> picks[u]] is a record: an email to u containing these posts.

Read it line by line. Send can only run once the send time has passed. If Plunk already knows the key, it replies with a 409 and nothing is delivered. Otherwise, the email goes out. Either way, Plunk remembers the key, and Barista marks the posts as sent. That last line is the one to watch. The real action can also end badly: Plunk delivers the email, then Barista crashes before recording anything. TLC tries that outcome too.

Now the property, in the same spirit as the cafe’s NeverOversold:

SentImpliesDelivered ==
  \A u \in Users : \A p \in sent[u] :
                       \* for every post marked as sent to u,
    \E i \in 1..Len(emails) : emails[i].to = u /\ p \in emails[i].posts
                       \* there's a delivered email to u containing it

In plain English: Barista’s belief must match the truth. If a post is marked as sent, an email really contained it.

I ran TLC. Guess what? Despite all the tests, despite the idempotency key I was paying 10x for, it failed on the first run. Every configuration failed, even the simplest one: no crash, no settings change. Here’s one of the counterexamples, in real times. Alice gets her email at 22:00 UTC:

An outage on May 20 eats Alice’s May 21 email. The catch-up send at 01:00 UTC uses key alice-20260521, so the regular send at 22:00 gets a 409, and its posts are marked as sent without being delivered.

Alice never gets her May 21 email. Its posts are marked as sent, so Barista will never offer them again. No error, no alert. And it happens 21 hours after everything recovered.

The fun part is that I never modeled an outage. Nothing in the spec says Barista can be down. But nothing forces Send to run on time either: in TLA+, the clock is just another action, and TLC is free to let it tick while Send waits. An outage, a slow deploy, a job stuck behind another one: for the model, it’s all the same. TLC tried every possible delay and found the one crossing midnight.

So what went wrong? Plunk did exactly what it promised. A 409 doesn’t mean “these posts were sent.” It means “something was already sent under this key.” My key was the day of the attempt, not the day the email was for. As long as a send ran on the day it was due, it didn’t matter. The moment one slipped past midnight, it did.

Should Barista skip the catch-up, then? No. Alice should still get her May 20 email. The catch-up was right; my reading of the 409 was wrong.

Ironically, I was obsessed with sending too many emails, and the very thing I was paying 10x for made me send too few, silently.

Would my tests have caught it? Honestly, no. I tested a crash after the ACK, and the idempotency key handled it. I would never have written a test where Send runs late, past midnight UTC, followed by a regular send the next evening. And that was exactly my fear in the first place.

The fix? One key per email instead of one per day. I re-ran TLC. Green.

The Future of Software Engineering?

In December 2025, Martin Kleppmann, the author of Designing Data-Intensive Applications, published a post with a bold prediction: AI will make formal verification go mainstream.

His argument is mostly about cost. Formal verification has always been expensive. Proving that seL4, an OS kernel of about 8,700 lines of C, was correct took around 20 person-years. For most systems, a bug was cheaper than the proof that would have prevented it. But coding agents are getting good at writing proofs. And a wrong proof isn’t dangerous: the checker rejects it, and the agent tries again.

One of the issues with TLA+ has always been making sure the spec is accurate. A TLA+ spec is a model, and a model is only as good as its abstraction. TLC checks the spec, not the code. The hard part is making sure the spec describes what the code actually does.

But with the rise of coding agents, especially over the last few months, I feel like this gap is shrinking. An agent can read the code and draft the spec, keep both in sync when the code changes, and turn a counterexample into a failing test against the real code.

At Google, I spent a lot of time exploring formal verification, especially on convoluted logic: loops with several paths, retries, error codes. On many occasions, I found bugs despite significant test coverage. Back then, though, writing and maintaining a spec was a real investment, so it was reserved for the parts that truly justified it.

That’s what’s changing. When a spec costs an afternoon instead of weeks, the question is no longer “is this part critical enough to deserve a spec?” It becomes “why not?”

Does it mean software will be bug-free? No. As Kleppmann also points out, the hard part moves to the specification itself: are we checking the properties we actually care about? That’s the validation question from earlier.

But think about what it took to find Barista’s bug: a property of a few lines, and a tool patient enough to try every delay, every order, every midnight.

Now extend that. Maybe that’s what software engineering becomes: less time on how the code achieves something, more time on what must hold no matter what. Alice never receives the same email twice. Alice eventually receives her daily email. We write those down; agents write the code and the spec; tools check that the properties hold. Kleppmann compares it to compilers: we don’t read the machine code they produce, and maybe one day, we won’t read the code agents produce either.

Will we get there? I don’t know. But it might be worth exploring in your own system: write down its invariants, and see whether a model can show you where they break.

If you want to see what this pipeline picks for you, give Barista a try. Describe what you like to read, and your first email lands in your inbox in seconds. It’s free (one post a day), and every new account gets 7 days of the paid plan to try more.

Comments

Ready for more?