My Tests Were Green. My Verification Tool Wasn't. — Igel Data

← All articles

Every unit test passed. The transaction suite was green. I had tests for concurrent writes, for crash recovery, for corrupted logs. By any normal standard, the database was done.

Then I pointed a small verification tool at it, ran a workload that just moves money between bank accounts, and it failed in seconds.

This is the story of the two bugs it found — both invisible to my tests, both the same underlying mistake wearing two different masks — and why “the tests pass” and “the system is correct” are not the same claim.

The database is IgelDB, a small embedded key-value store. But the real subject of this post is the tool that broke it, and the style of testing that makes bugs like these fall out.

Tests check what you thought of. Verification checks what you didn’t.

A unit test is a sentence you write in advance: “when I do X, I expect Y.” It’s only as good as your imagination. If you didn’t think to write down a scenario, the test can’t catch it.

Concurrency bugs live exactly where your imagination runs out. They appear only under specific interleavings of parallel operations — orderings you never explicitly wrote a test for, because there are astronomically many of them.

Verification flips the approach. Instead of asserting specific outcomes, you:

Generate random concurrent operations from many clients.

Record the full history of what happened.

Check that the history obeys a property that must always hold — no matter the interleaving.

You don’t predict the bug. You define what “correct” means, throw chaos at the system, and let the checker find any history that violates correctness. This is the idea behind Jepsen, the well-known distributed-systems testing framework. I wanted that idea in a lighter form for embedded libraries, so I built a scoped-down version — call it Jepsen Lite.

The workload that broke IgelDB is the classic one: a bank .

The bank workload: correctness you can count

Picture a set of bank accounts, each holding a balance. Many clients run concurrently, each doing the same kind of transaction: take some money from account A and move it to account B.

graph LR<br>subgraph "Many clients, in parallel"<br>C1["transfer $10A → B"]<br>C2["transfer $5C → A"]<br>C3["transfer $20B → D"]<br>end<br>C1 --> DB[(IgelDB)]<br>C2 --> DB<br>C3 --> DB

Every transfer only moves money — it never creates or destroys it. So there is one property that must hold at every instant, no matter how many transfers run in parallel:

The total of all balances never changes.

That’s the whole trick. The bank workload turns a subtle correctness question into arithmetic. If the total ever drifts, some transfer’s write was silently lost — and the checker just has to add up the numbers.

I ran it. The total drifted. Money vanished.

What the transactions were supposed to guarantee

IgelDB’s transactions use snapshot isolation , the same model most databases use by default. Two rules matter for this story:

1. A transaction reads from a consistent snapshot. When a transaction starts, it sees a frozen picture of the database as of that moment. Other transactions committing afterward don’t disturb its view.

graph TD<br>T["Transaction startstakes a snapshot"] --> R1["reads balance A = $100"]<br>R1 --> R2["reads balance B = $50"]<br>R2 --> Note["Even if others commit now,this transaction still sees $100 / $50"]

2. If two transactions write the same key, one must lose. This is what stops lost updates. If two transfers both touch account A at the same time, they can’t both blindly commit — the second one to commit must notice the conflict and be rejected (then retried).

graph TD<br>subgraph "Correct behavior"<br>A1["Tx1: change A"] --> A2["Tx1 commits ✓"]<br>B1["Tx2: change Asame time"] --> B2["Tx2 sees conflictrejected, retries ✓"]<br>end

If either rule breaks, transfers can lose money. Both rules broke — in two different places.

Bug #1: the gap between “committed” and “visible”

To detect a write-write conflict, a committing transaction asks: “has anyone else modified the keys I’m about to write, since my snapshot?” If yes, it’s a conflict.

The problem was when a freshly committed write becomes findable by that question.

Committing a transaction in IgelDB happens in two stages:

Confirm the commit: assign it an order number and write it to the durable log.

Apply it: make it visible to reads, a moment later, on a background worker.

There’s a gap between those two stages. And the conflict check looked for other transactions’ writes using the read path — which only sees applied writes. So during the gap, a committed-but-not-yet-applied write was invisible to the conflict check .

sequenceDiagram<br>participant A as Transaction A<br>participant Log as Durable log<br>participant Mem as Visible state<br>participant B as Transaction B

A->>Log: confirm commit (write to A)<br>Note over Mem: not applied yet<br>B->>Mem: conflict check: "did anyone write A?"<br>Mem-->>B: "no" (A's write not visible...