My reading app's conflict dialog fired 170 times, and in 106 of them the other side was me: how many bugs can a sync protocol with one user hide?

I wrote a little web e-book reader. It's on my phone and my tablet, and it keeps my place in sync between the two.

Its database says the conflict dialog has been resolved 170 times. In 106 of those, the write right before the conflict came from the same device.

So 62% of the "conflicts" were one device arguing with itself.

Nobody uses this thing but me, on two devices. I assumed sync at that scale might fail in some rare corner, at worst. Then I ran it through a formal verification tool. All 8 rules I wrote down had counterexamples, and the fastest one showed up in under a second.

If you only want the two formulas, read sections 2 and 5. If you want to know how to read a "verification passed" report, read section 6. After my fix, one of my own checks passed without testing anything.

1. How the reader syncs

The rules aren't complicated. Here they are, straight from the code:

• The server stores one progress row per book, with a version number. A client reports "the version I have is N" when it writes. If that matches, the write goes through and the version goes up by one. If not, the server returns 409 along with its current value, and the front end pops a conflict dialog
• After you turn a page, the client waits 1.2 seconds before pushing, so fast page flips collapse into one write. That wait is the debounce
• When the tab goes to the background or the screen locks, the browser's sendBeacon fires off the current position. A beacon is fire-and-forget. You never get to read the response
• While offline, progress goes into a local outbox, one entry per book, pushed when the network comes back
• Every successful write is also mirrored to a KOReader sync server (KOSync) running on my NAS, so my e-ink reader stays in step. Each time a book opens, the server checks KOSync for anything newer and pulls it back if so

Each rule looks reasonable on its own. Every problem showed up where they meet.

2. The 106 times I argued with myself

First, where that 62% comes from.

Turn a page, and the debounce starts its 1.2-second countdown. Lock the screen inside that window, and the beacon writes the position first, taking the server from v1 to v2. But a beacon can't read its response, so the phone still thinks it holds v1.

Unlock, and the still-pending debounce fires as usual, claiming v1. The server is at v2, so it answers 409. Up comes the conflict dialog, and the device name in its "cloud" column is this very phone.

I reproduced it with the real code in a browser. Here's an excerpt of the output:

1) phone reads to 40% → { f: 0.4011, v: 1 }
2) after lock-screen beacon → { f: 0.4521, v: 2 }
3) back to foreground: conflict dialog shown = true  "cloud" label = cloud (iOS Safari)

Turn a page, lock the phone. I do that every day.

Here's the first number you can take away. It works for anything that syncs with version numbers:

self-conflict ratio = conflicts where the previous write came from the same device ÷ total conflicts
mine: 106 ÷ 170 ≈ 62%

A high ratio means your conflict detection is catching yourself. Real multi-device conflicts should happen when you switch devices. Two consecutive writes from the same device shouldn't conflict at all.

One caveat up front: the lock-screen mechanism above explains this shape, but I didn't attribute all 106 one by one. Other paths could be mixed in, like the adopt-the-server-version bug in section 4.

3. I wrote the rules as a model, and TLC took under a second

TLA+ is a language for describing a system as state plus actions. TLC is its model checker: it walks every combination of actions in every order and looks for a path that reaches a state you said must never happen. Basically, brute force over interleavings.

I modeled two devices, the server, the outbox, KOSync, and requests in flight, and annotated each action with the code lines it came from. I kept it small: two devices, three progress levels, each device reads at most twice, opens and closes the book once, and drops the network at most twice.

Then I wrote 8 "this must never happen" rules, for example:

• A device that never saw a further position writes the server back to an earlier one
• A newer outbox entry gets overwritten by an older one or deleted by mistake
• On close, the final position reaches neither the server nor the outbox
• A device conflicts with its own previous write

I ran each one separately. All 8 were violated. I also split one of them by source into three sub-rules, and two of those were violated too, for 10 violations in total:

Rule	States generated	Counterexample length	Time
Conflicts with itself	567	4	under 1 s
Position lost on close	494	4	under 1 s
Written back to earlier position	25,466	7	under 1 s
Outbox overwritten	367,580	8	1 s
KOSync pulls progress back	2,024,203	9	3 s

The shortest counterexamples were 4 steps. For the self-conflict rule that's roughly: turn page, lock, unlock, push. I walk those 4 steps every day and never noticed they were a counterexample.

Two small gotchas during setup. TLC needs Java 11 or newer, and my machine only had 8, so I grabbed a portable JDK 21. And TLC's state directory eats disk: the bigger runs wrote around 7G per round. It cleans up afterward, but the peak can push an almost-full disk over the edge. My root partition hit bottom that day, and TLC was one of the culprits.

4. 10 counterexamples, 7 real bugs

TLC gives you counterexamples to the model. I wrote the model, and if I wrote it wrong, it reports anyway. So every one had to be replayed against the real code.

I built a small harness. The server's sync code was cut out verbatim by markers, not a single line of logic copied by hand. KOSync became a local fake with the same wire format. The front end ran straight from the repo source. Playwright drove two isolated browser contexts as the two devices, really turning pages, going offline, switching to the background. The outputs below are excerpts, with device names shortened.

Deduplicated by root cause, the 10 violations came down to 9. Seven reproduced, two didn't.

The two nastiest:

After a conflict, the next write overwrites the other device. On a 409, the front end quietly adopted the server's version number. The dialog is still open and you haven't chosen anything, but you turn another page, the version matches now, and the write succeeds. The tablet's 60% gets overwritten by the phone's 30.6%:

5) phone turns a page at 30% → conflict dialog = true  row { f: 0.6008, v: 4, dev: 'tablet' }
6) phone turns another page (dialog untouched) → { f: 0.3059, v: 5, dev: 'phone' }

The conflict dialog is a modal, but keyboard and gamepad page turns ignore it completely.

Offline reading gets overwritten when you reopen the book. On the subway with no signal, I read from 30% to 50%. Out of the station, signal back, I open the book. The code pulls from the server first (30%) and jumps there, and only then drains the outbox (50%). The server now says 50%, but the screen is still at 30%. Turn one page and 30.4% gets written. The 50% is gone:

4) reopen book: screen shows 30.1 % ; row { f: 0.5008, v: 2 }
5) turn a page from the screen position: screen 30.4 % ; row { f: 0.3036, v: 3 }

The two that didn't reproduce came from my model being looser than the code. I let the model open books while offline, and TLC followed that path to "an offline open starts from the beginning." The other one's shortest path also went through an offline open. The real code can't even load the bookshelf offline. It just says "book not found," so that path doesn't exist. No bug there, but it did tell me something else: offline reading only works if the book was already open when the connection dropped.

Of the 9, 7 were real and 2 were fake. I was tempted to report all 10 as bugs at first. It looked better.

5. Cross-clock comparison: I thought clock drift was the risk

For the KOSync one, I first assumed the problem was the clocks.

The pull-back rule goes like this. If the KOSync record's timestamp is more than 1.5 seconds later than the server row's update time, and it was written by a different device, treat it as "newer from elsewhere" and pull it in. The KOSync timestamp comes from the NAS clock and the row's comes from another machine's clock, so two clocks are being compared.

My first move was to measure clock skew. The two were within ±20 ms of each other, nowhere near the 1.5-second margin.

It broke anyway. Here's the sequence I reproduced:

1) phone PUT 30%            → server v1, mirror to KOSync (stuck 4 seconds on the NAS)
2) tablet PUT 60%           → server v2, its KOSync mirror lands first
3) phone's stale write lands → KOSync now says 30%, with the newest timestamp
4) any device opens the book → {"fraction":0.3,"version":3,"deviceId":"phone"}

A stale write that lands late carries a fresh timestamp. No clock drifted here. Two requests simply arrived in the wrong order.

You can size this window from two constants in the code. Say the phone's mirror write spends d seconds in flight, and the tablet writes g seconds after the phone. The pull-back happens when the stale write lands more than 1.5 seconds after the tablet's write:

d > g + 1.5
d tops out at the mirror timeout, 5 seconds
⇒ if two devices write less than g < 5 − 1.5 = 3.5 seconds apart, progress can get pulled back

In general:

regression window = max allowed latency on the write path − safety margin in the timestamp comparison

When the margin is smaller than the latency ceiling, the window exists no matter how accurate your clocks are. The 3.5 seconds is an upper bound derived from the constants. I never measured how fast the NAS normally responds, so I can't give you a probability, only that it isn't zero.

The fix didn't touch the margin either. Values the server itself mirrored to KOSync are never pulled back in. Only records written by the actual e-ink reader are. And mirror writes are queued per book, pushing only the latest one.

6. How to read a "0 violations"

This section is for when you're reading someone else's verification report. After my fix, my own "pass" nearly fooled me.

With the fix in, I reran TLC on the fixed model. Each of the 7 rules ran for 300 seconds and covered over 40 million distinct states, with no counterexample. On the real-code side, a checker passed all 28 items.

Sounds solid. Pull it apart in three places:

Did it finish? 300 seconds was a cap I set. It stopped at the cap, and the state space wasn't exhausted. Before the fix, one rule ran for 15 minutes and generated 270 million states without a counterexample, and I stopped that one by hand too. Zero violations from an unfinished TLC run means "didn't run into one in this many states." That's a long way from a proof.

Is the path reachable in the model? After the fix, "KOSync pulls progress back" passed in the model. When I went back and checked reachability, I found that the fix added "don't pull back values we mirrored ourselves," and both devices in the model were my own reader app. No e-ink reader. The pull-back logic never executed in the model even once. That rule passed vacuously: nobody ever walked the path it was checking. The real e-ink pull-back ended up covered by a real-code test case.

Can the checker tell good from bad? Alongside those 28 items, I fed the same checker the pre-fix code, and it reported 10 FAILs. Skip that step and 28/28 tells you nothing. A checker that always says green also gets 28/28.

So when you see "formally verified," ask three things. Did it finish, or stop at a cap? Did the model ever actually reach the path being checked? Does the same check go red on a version known to be buggy? If you can't answer any one of them, put a question mark on that "pass."

7. What I didn't get to

• The model is tiny: 2 devices, 3 progress levels, at most 2 reads per device. I don't know what longer sequences hide
• I only modeled zero clock skew. With skew above 1.5 seconds, KOSync has another path ("lost push plus drift") that I neither explored nor reproduced. Measured skew is ±20 ms, so it's not urgent
• Screen locks were simulated with Playwright's visibilitychange, network drops with setOffline. Real iOS Safari freezing background tabs can only be worse, not better
• The KOSync case used a 4-second delay I injected. I don't have the NAS's real latency distribution, so section 5 gives an upper bound on the window, not a probability
• I didn't attribute the 106 self-conflicts one by one to specific mechanisms
• Multiple tabs on the same device, and the full interleaving of the reader's exclusive-session logic with conflicts, were not modeled

8. Next time you write sync logic, go through this in order

1. Look at your conflict log and compute the self-conflict ratio. If it's over half, don't chase multi-device issues yet. Check your debounce, your beacons, and when your version number advances
2. For any write that fires without reading the response, ask: when it succeeds, who updates the local version number?
3. On a conflict, don't quietly adopt the server's version. Hold further writes until the conflict is resolved
4. At moments like opening a book or coming back online, push the local backlog first, then pull the remote
5. Anywhere you compare timestamps across machines, compute "max latency − safety margin." If it's above zero, don't use timestamps to decide which write is newer
6. Write the rules up in TLA+ and run them. The shortest counterexamples are often just four or five steps, out in seconds. Replay each one against real code before you call it a bug
7. For a "0 violations" after a fix, add three things: did it finish, is the path reachable, does the checker go red on the old code
8. Put TLC's state directory on a disk with room to spare