Never twice... but maybe never

Formal verification has been following me around the internet this month. My friend and ex-colleague Rory wrote about using Claude to build a deterministic simulation harness for a message broker: a few weeks of work, nicely squashed into a day. Boris Cherny posted about it too.

Model checking has been around for decades. SPIN came out in the late 80s, and TLA+ and TLC are from the late 90s. Using them has always felt out of reach to me. There's new, and often dense, notation to learn: and even when you've cracked that, how do you know your spec describes your system, rather than something that just looks like it?

Coding agents have changed that for me. They can turn production code into a first draft of a spec, so the notation is much less of a wall. They can also walk me through the traces step by step, which is probably the bit where I'd previously have given up.

I tried it on a real piece of our codebase, and it found something. This post tells you how.

The property

Formal verification starts with a statement about your system that should always be true: this is a property. "Two people can't book the same seat on a flight", or "every order is eventually either shipped or refunded". Write that sentence precisely, describe how the system behaves, and a tool can check that the property holds in every state the system can reach, not just the ones your tests happen to try.

When a build finishes testing, we post a summary to the customer's Slack channel: which tests passed, which failed, and why. The one thing it must never do is post twice. A duplicate summary looks broken, and people ignore things that look broken. Our property: "When a build finishes, its summary is posted to Slack exactly once".

If 'exactly once' sets off alarm bells, you'd be right. It sounds trivial until you count the ways a summary can be triggered:

• When a test run finishes, our root cause analysis process checks whether it was the last one, and if so, generates a summary.
• Cancelling a test run does the same.
• The summary is sent from a Cloudflare workflow, which retries a step if the Worker dies halfway through.
• If there's a Cloudflare outage, and we can't start a workflow, we send the message inline.
• You can rerun a test after the summary has gone out, which changes the build's results and starts a fresh workflow.

All of these can happen concurrently, in any order, which is good fun for us as software engineers. What stops them all posting is one conditional update. Before posting, each sender tries to claim the build by setting buildSummaryNotifiedAt, but only if it's still NULL. The database lets exactly one of them win, and only the winner posts:

const result = await db
  .updateTable("build")
  .set({ buildSummaryNotifiedAt: now })
  .where("id", "=", buildId)
  .where("buildSummaryNotifiedAt", "is", null)
  .executeTakeFirst();

return result.numUpdatedRows !== 0; // Did we win?

We have unit tests for this, but a unit test only checks one sequence of events: the one you thought of. That's probably the happy path, or one of the obvious failure modes.

How could we test every possibility? Enter the model checker.

Three ideas you need

First, a bit of theory. It's necessary, but don't worry, there's not much of it:

• A model is a deliberately small copy of your system. Its state is a handful of variables, and its actions change them. Concurrency just means the actions can happen in any order. You keep what decides correctness, like whether the build has been claimed and how many messages exist. Everything else goes, like what the message says and how Slack formats it.
• Safety vs. liveness. A safety property says something bad never happens, like "never two messages". A liveness property says some desired outcome eventually happens, like "the message gets sent". They fail in very different ways and, spoiler alert, that's the whole plot of this post.
• A model checker tries everything. It starts from the initial state, applies every possible action, and keeps going until it's visited every reachable state. If one of them breaks your property, it shows you the exact steps that got there. This is called a counterexample.

If you're wondering: yes, there's a catch. The checker can only try everything if "everything" is finite, so you choose the limits: two test runs instead of fifty, one rerun instead of unlimited. Inside those limits, it checks every combination. That's less of a cheat than it sounds: the small scope hypothesis says most concurrency bugs show up with just a few actors.

Why Quint?

I used Quint for this. It uses the same underlying logic as TLA+, but with syntax that'll look familiar if you've written TypeScript. It installs from npm, and it comes with two ways to check things:

• quint run: a random simulator. It only needs Node, and is good for a quick sanity check.
• quint verify: hands the spec to a real model checker (Apalache or TLC) to check every state. It needs Java (sorry).

If you want to follow along, save the full spec from the end of this post as buildSummary.qnt, then run:

npx @informalsystems/quint typecheck buildSummary.qnt
npx @informalsystems/quint run buildSummary.qnt --invariant=atMostOnce

Writing the model

This is the bit where usually I would have dropped out of the 'funnel'.

I asked Claude to read our build summary code and draft a model of it. Then I got it to walk me through each action, so I could check it matched something the code can genuinely do.

Here's the state:

var runs: str -> RunStatus        // each test run: Pending or Done
var version: int                  // stands in for the build's results hash
var triggers: int                 // "was it the last run?" checks to come
var senders: (Kind, int) -> Phase // workflow instances and inline fallbacks
var claimed: bool                 // buildSummaryNotifiedAt IS NOT NULL
var slackMessages: int            // messages in the customer's channel

Then, one action per thing that can happen in the system. The interesting one is the claim, which in our code is a UPDATE ... WHERE ... IS NULL query:

action claim(s) = all {
  senders.get(s) == Ready,
  if (noPending and not(claimed))
    all { claimed' = true, senders' = senders.set(s, Claimed) }
  else
    all { claimed' = claimed, senders' = senders.set(s, Finished) },
  // ...and every other variable stays the same
}

That apostrophe isn't a typo: a primed variable (claimed') means "the value in the next state". all { ... } means every line must hold. The other actions are things like postToSlack, slackRefuses (Slack returns a 429 or ok: false) and crash (the Cloudflare Worker dies mid-step, and a workflow retries the step from the top).

The key trick is non-determinism. When a trigger fires and nothing is pending, the code tries to start a workflow, but that can fail too. In the model, we don't decide which happens:

any {
  senders' = senders.put(instance, Ready), // starts, or already exists
  senders' = senders.put(inline, Ready),   // failed to start: send inline
}

any means "any one of these could happen", and it tells the model checker to follow every branch. This means you don't have to imagine all of the possible failure modes: you just have to state they're possible.

Finally, the two properties, written as plain booleans over the state. Quint calls these invariants, because they have to hold in every single state:

val atMostOnce = slackMessages <= 1

val settled = and {
  noPending,
  triggers == 0,
  senders.keys().forall(s => senders.get(s) == Finished),
}
val exactlyOnce = settled implies slackMessages == 1

exactlyOnce is how we sneak a liveness property in as an invariant: once the dust has settled, exactly one message has gone out.

Prove it

Now we've got our model, let's prove it:

npx @informalsystems/quint verify buildSummary.qnt \
  --backend=tlc --invariant=atMostOnce

Model checking completed. No error has been found.
12107 states generated, 3668 distinct states found, 0 states left on queue.
[ok] No violation found (419ms).

That's every reachable state in our small world (all 3,668 of them) checked in under half a second. No ordering of finishes, cancels, retries, crashes, reruns and fallbacks produces a second message.

Break it

Of course, this isn't where I started: the model checker failed first, and I got Claude to turn each counterexample into a unit test. That's really the point. Just like a test, a proof is only convincing once you've seen it say no. So let's break it: delete the guard by changing noPending and not(claimed) to just noPending, and run it again.

[violation] Found an issue (397ms).

It found a counterexample almost instantly. When I asked it to look for each route separately, it turned up three different ways to post twice.

The first is a retry after success. The workflow claims, posts to Slack, and then the Worker dies before the step's result is saved. The retry claims again, and posts again. This is why our code claims inside the same step as the post, as late as possible.

The second is a rerun. The summary goes out, the customer reruns a test, and the new results start a fresh workflow, which posts too.

The third is the fallback. Two analyses finish at the same moment: one starts the workflow, the other fails to start it, and sends inline instead.

Each of those is a plausible Tuesday in production, and I wouldn't have written a unit test for any of them.

Find the gap

Now the liveness property:

npx @informalsystems/quint verify buildSummary.qnt \
  --backend=tlc --invariant=exactlyOnce

[violation] Found an issue (325ms).

The shortest counterexample goes like this:

1. Run B finishes, but A is still pending, so nothing starts.
2. Run A finishes. It's the last one, so the workflow starts.
3. The workflow claims the build.
4. Slack returns a 429. We log a warning and return. The build is claimed, so nothing will ever try again.

There's also a second route that doesn't need Slack to misbehave at all: the Worker dies between claiming and posting, and the retry finds the claim already taken, so it bows out politely.

This isn't really a bug in our code. It's a trade-off you can't dodge:

• Claim, then post gives you at most once. A failure in between loses the message.
• Post, then claim gives you at least once. A failure in between sends it again.
• Exactly once needs the receiver to deduplicate for you, by recognising a repeat and ignoring it. Slack's chat.postMessage doesn't take an idempotency key, so that isn't on offer.

We chose at-most-once, which we think is the right call for a notification: a duplicate is something every customer sees, while a missing summary still leaves the results on the build page.

What a model can't tell you

The big one: it checks the model, not the code. If someone changes the TypeScript and not the spec, the proof quietly stops being about our system. A spec in a blog post doesn't drift, but a spec in a repo does.

Models also simplify. Ours treats the claim as one atomic step, but the real code checks for pending runs and then updates, as two separate statements. A run queued between the two can see a summary posted while it's still pending. It's harmless (the message is edited when the run finishes), but the model can't see it, because we left it out.

And it's a small world. I'm fairly confident a third test run adds nothing new, but that's the small scope hypothesis talking, not a proof.

Wrapping up

The whole exercise took a couple of hours, and most of it was me reading traces and asking "is this really what our system does?"

If you've got a piece of code out there with a comment like "This is safe because...", that's a great place to start. Hopefully this post has given you a new tool for your belt.

You can find out more about Semaloop, and the build summaries that started all this, at semaloop.com.

The full spec

module buildSummary {
  pure val RUNS = Set("a", "b")
  pure val MAX_VERSION = 4  // bounds reruns, so the state space is finite

  type RunStatus = Pending | Done
  type Kind = Workflow | Inline
  type Phase = Ready | Claimed | Posted | Finished

  var runs: str -> RunStatus
  var version: int
  var triggers: int
  var senders: (Kind, int) -> Phase
  var claimed: bool
  var slackMessages: int

  def noPending = RUNS.forall(r => runs.get(r) == Done)

  action init = all {
    runs' = RUNS.mapBy(_ => Pending),
    version' = 0,
    triggers' = 0,
    senders' = Map(),
    claimed' = false,
    slackMessages' = 0,
  }

  action finishRun(r: str): bool = all {
    runs.get(r) == Pending,
    runs' = runs.set(r, Done),
    version' = version + 1,
    triggers' = triggers + 1,
    senders' = senders,
    claimed' = claimed,
    slackMessages' = slackMessages,
  }

  action rerun(r: str): bool = all {
    runs.get(r) == Done,
    version < MAX_VERSION,
    runs' = runs.set(r, Pending),
    version' = version + 1,
    triggers' = triggers,
    senders' = senders,
    claimed' = claimed,
    slackMessages' = slackMessages,
  }

  action handleTrigger: bool = {
    val instance = (Workflow, version)
    val inline = (Inline, senders.keys().size())
    all {
      triggers > 0,
      triggers' = triggers - 1,
      if (not(noPending)) senders' = senders
      else any {
        senders' = if (senders.keys().contains(instance)) senders
                   else senders.put(instance, Ready),
        senders' = senders.put(inline, Ready),
      },
      runs' = runs,
      version' = version,
      claimed' = claimed,
      slackMessages' = slackMessages,
    }
  }

  action claim(s: (Kind, int)): bool = all {
    senders.get(s) == Ready,
    if (noPending and not(claimed))
      all { claimed' = true, senders' = senders.set(s, Claimed) }
    else
      all { claimed' = claimed, senders' = senders.set(s, Finished) },
    runs' = runs,
    version' = version,
    triggers' = triggers,
    slackMessages' = slackMessages,
  }

  action postToSlack(s: (Kind, int)): bool = all {
    senders.get(s) == Claimed,
    senders' = senders.set(s, Posted),
    slackMessages' = slackMessages + 1,
    runs' = runs,
    version' = version,
    triggers' = triggers,
    claimed' = claimed,
  }

  action slackRefuses(s: (Kind, int)): bool = all {
    senders.get(s) == Claimed,
    senders' = senders.set(s, Finished),
    slackMessages' = slackMessages,
    runs' = runs,
    version' = version,
    triggers' = triggers,
    claimed' = claimed,
  }

  action stepCompletes(s: (Kind, int)): bool = all {
    senders.get(s) == Posted,
    senders' = senders.set(s, Finished),
    slackMessages' = slackMessages,
    runs' = runs,
    version' = version,
    triggers' = triggers,
    claimed' = claimed,
  }

  action crash(s: (Kind, int)): bool = all {
    Set(Claimed, Posted).contains(senders.get(s)),
    senders' = senders.set(s, if (s._1 == Workflow) Ready else Finished),
    slackMessages' = slackMessages,
    runs' = runs,
    version' = version,
    triggers' = triggers,
    claimed' = claimed,
  }

  action step = any {
    nondet r = RUNS.oneOf()
    any { finishRun(r), rerun(r) },
    handleTrigger,
    all {
      senders.keys().size() > 0,
      nondet s = senders.keys().oneOf()
      any {
        claim(s), postToSlack(s), slackRefuses(s),
        stepCompletes(s), crash(s),
      },
    },
  }

  val atMostOnce = slackMessages <= 1

  val settled = and {
    noPending,
    triggers == 0,
    senders.keys().forall(s => senders.get(s) == Finished),
  }
  val exactlyOnce = settled implies slackMessages == 1
}