Martin Kleppmann
What deceives you isn't the code. It's the words you were handed to describe it

One strange thing

Pull up the archive page at martin.kleppmann.com and read it from the bottom: 126 posts across nineteen years. In the first 70 — the years 2007 to 2009 — exactly one touches databases.

The other sixty-nine are these: "Usability aspects of gas cookers." "Train ticket machines — UK vs. Germany (Part 1)", followed five months later by Part 2, and five months after that by "Update on German train ticket machines." "Find my nearest toilet, curry, whatever." "Screenshots from Windows Vista Update." "Yes/No/Cancel causes Aspirin sales to soar."

In 2008 alone he published 31 posts. In all of 2023 he published none.

The man who wrote those went on to write Designing Data-Intensive Applications (DDIA) — the book a generation of engineers uses to think about databases, which Jay Kreps, the creator of Kafka, calls "the best book for understanding distributed systems" of the last decade.

It looks like a total career change. He never changed subject.

A German ticket machine that makes you press the wrong button, and a database where "repeatable read" means three different things in three products, are to him the same bug. That isn't my analogy — he wrote the sentence himself in 2014, and its subject is ACID transaction isolation:

The levels basically have no intuitive meaning, because they are an incredibly leaky abstraction — they are defined by implementation detail, not because someone thought they'd make a great API. And that's also why they are so hard to understand.Hermitage: Testing the “I” in ACID, November 2014

That is a usability complaint. About ACID.

Who he is

Martin Kleppmann, German, long based in Cambridge. Two startups sold (Go Test It to Red Gate in 2009, Rapportive to LinkedIn in 2012), then LinkedIn, working on the stream processing framework Apache Samza. In 2014 he quit and lived for a full year with no income, on savings, writing the book. He is now an Associate Professor in Cambridge's Department of Computer Science and Technology — with a detour as a research fellow at TU Munich (2022–2023) — working on local-first collaboration software and security protocols. The second edition of DDIA, co-authored with Chris Riccomini, appeared in March 2026: 670 pages.

One detail with a picture in it: on his otherwise austere academic homepage, tucked between the papers, is a line noting that he composed a musical, Die Türme des Februar, premiered in 2007 with a cast of 150. Another: he published his book royalties down to the dollar on his blog, so that other people could work out whether the deal is worth taking.

The blog is alive, but the decline is dramatic: 20 posts in 2007, 31 in 2008, 19 in 2009 — then down to 1 in 2018, zero in 2023, and 1 in 2025 (8 December). Not dormant: he has four conference talks scheduled for 2026, including an SRDS keynote. It's a prolific blogger turning into an academic who posts once a year.

Glossary

What he is fighting

In 2014 he was writing the transactions chapter of DDIA. He wanted to explain isolation levels well enough that a reader could tell whether their own code was safe at a given level. He got stuck, because he discovered that the words themselves are empty.

He didn't route around it. He did something laborious instead: he wrote a test suite called Hermitage, translating each concurrency anomaly defined in the research literature into concrete SQL, and ran it against every isolation level of PostgreSQL, MySQL, Oracle and SQL Server, to see which ones actually held.

The results: three of them have a level called "repeatable read" and it means something different in each. Oracle's "serializable" isn't serializable, it's snapshot isolation. SQL Server's default lock-based modes look remarkably like System R in 1975.

But the sharpest moment is at the top of the piece. He opens with a real incident: a Bitcoin exchange nearly bankrupted by a race condition on outgoing payments — an attacker made many concurrent withdrawals and got around the balance check. Internet commenters agreed: if you're dealing with money, use an ACID database. Then he writes:

Yes, you read that right. Those databases — the ones that have probably processed the vast majority of commercial transactions over the last 20 years — do not by default guarantee that your transactions are protected from race conditions.Hermitage: Testing the “I” in ACID, 2014

He also issues a challenge anyone can run on the spot: find a colleague who can explain, off the cuff and without looking at the docs, the difference between "repeatable read" and "read committed", with an example where they behave differently. He bets you can't — unless that person used to work on database internals.

That is the thing he has really been fighting for a decade, and it is far more specific than "distributed systems are hard": what makes you believe false things is usually not wrong code, but badly designed words that get read as promises. "Repeatable read" sounds like a guarantee; it describes the side effects of somebody's 1975 implementation. "ACID" sounds like a safety certificate; its C has nothing to do with the C in CAP. "It's a CP system" sounds like an architectural judgement; it is a pile of incompressible differences crushed into one bit.

His ideas, told as how he found them

1. Your database is neither CP nor AP. It's just "P"

Spring 2015. "We're CP", "they're AP" had become the common language of architecture discussions, prompted by a popular introductory post advising newcomers to critique systems using the CAP theorem. Kleppmann agreed with every other point in it and not this one — and then did something almost nobody does: he went back to the original proof and checked the words one at a time.

Four landmines. Consistency in CAP means linearizability, and "it has got nothing to do with the C in ACID, even though that C also stands for consistency." Availability is defined as every request received by a non-failing node returning a non-error response — every node; many systems marketed as "highly available" (meaning: little downtime) don't meet it. Partition tolerance, which he calls terribly mis-named, just means you're communicating over an asynchronous network that may delay or drop messages — the internet and every datacenter have that property, so you have no choice in the matter. And the worst one: the system model of the theorem is a single read-write register, full stop. Multi-object transactions are out of scope. Latency is never mentioned at all — a CAP-available system is allowed to be arbitrarily slow and still count as available.

Mathematics requires precision. The proof only holds if you use the words with the same meaning as they are used in the proof.Please stop calling databases CP or AP, 2015

Then comes the real weight of the piece: he tries to classify real systems one by one, and cannot place a single one. A single-leader replicated relational database — the standard production setup — can't write when partitioned from the leader, so it isn't CAP-available, whatever the marketing says about high availability; but let it read from an async follower and it isn't linearizable either. Neither. Databases with snapshot isolation are deliberately non-linearizable, because enforcing it would cut concurrency. MongoDB: also neither.

The finale is ZooKeeper, everybody's textbook case of "it runs a consensus algorithm, so obviously CP". He read the documentation: ZooKeeper does not do linearizable reads by default — each client reads from the node it happens to be connected to, even when newer writes exist elsewhere. You can get linearizability by preceding a read with sync, but it costs performance, so it isn't the default. Writes need a majority quorum, so nodes on the minority side of a partition are up but can't process writes — not CAP-available either. And version 3.4.0 added a read-only mode letting the minority side keep serving reads, which is CAP-available.

They are neither “CP” nor “AP”, they are just “P”, whatever that means. (Yes, the “two out of three” formulation does allow you to pick only one out of three, or even none out of three!)Please stop calling databases CP or AP, 2015

And his irritation with the ZooKeeper case runs in the opposite direction too, which is the most revealing thing about what he actually cares about: calling ZooKeeper "not consistent" just because it isn't linearizable by default badly misrepresents it — it provides atomic broadcast plus causal session guarantees, stronger than read-your-writes, monotonic reads and consistent prefix reads combined. His real point is that one bit cannot hold these differences, and people are making architecture decisions with that one bit: ZooKeeper's "AP" read-only mode still gives a total ordering of historical writes, vastly stronger than the "AP" of Riak or Cassandra — "so it's ridiculous to throw them into the same bucket."

Finally, his posture. He doesn't say "and here is my better taxonomy." He says that if CAP doesn't apply, you have to think through the trade-offs yourself; you can reason with your own definitions, and "you're welcome to prove your own theorem. But please don't call it CAP theorem, because that name is already taken." Then he scatters a dozen paper links and tells you to go read them. He also wrote a peer-reviewed paper of his own, A Critique of the CAP Theorem.

2. Redlock: an algorithm that quietly made "clocks are roughly right" an axiom

Early 2016, still doing background research for the book, he came across an algorithm called Redlock on the Redis website: fault-tolerant distributed locks via majority voting across five Redis instances, with the page inviting feedback from people who are into distributed systems.

The algorithm instinctively set off some alarm bells in the back of my mind, so I spent a bit of time thinking about it and writing up these notes.How to do distributed locking, 2016

He adds the practical pressure: there are already over ten independent implementations, and nobody knows who is relying on it for what.

His first cut isn't technical, it's a classification, and it determines the shape of the whole essay. What is the lock for? You tell by asking: what would happen if the lock failed? Locking for efficiency means failure costs you five cents more to AWS, or a user getting the same email twice. Locking for correctness means failure gives you "a corrupted file, data loss, permanent inconsistency, the wrong dose of a drug administered to a patient, or some other serious problem."

Then the blow. He shows a piece of code anyone would write — acquire lock, read file, modify, write back, release — and says: even if you have a perfect lock service, this code is broken. Client 1 acquires the lease (a lock with a timeout, which is good design, since otherwise a crashed client holds the lock forever), and then its garbage collector begins a stop-the-world pause that outlasts the lease. Client 1 wakes up knowing nothing about this and goes ahead with its write — while client 2, having acquired the lock, is already at work. The data is corrupted. HBase really had this bug.

Nor can you fix it by checking the expiry just before writing, because GC can pause your thread at any point, including the point that is maximally inconvenient for you: between that last check and the write. And for anyone feeling smug because their language has no GC, he closes off the escape:

Maybe your process tried to read an address that is not yet loaded into memory, so it gets a page fault and is paused until the page is loaded from disk. Maybe your disk is actually EBS, and so reading a variable unwittingly turned into a synchronous network request over Amazon's congested network. […] Maybe someone accidentally sent SIGSTOP to the process. Whatever. Your processes will get paused.How to do distributed locking, 2016

The fix is almost insultingly simple: a fencing token. Every time the lock service grants the lock it attaches a strictly increasing number. Client 1 gets 33 and pauses; client 2 gets 34 and its write succeeds; client 1 wakes up and writes with 33 — and the storage server, remembering it has already processed 34, rejects it. Note where the responsibility moves: the storage server has to actively check tokens and refuse ones that went backwards, but "this is not particularly hard, once you know the trick." With ZooKeeper as the lock service, the zxid already works as a token.

Redlock cannot produce that number. Its unique random value has no monotonicity; a counter on one Redis node dies with that node; counters on several nodes drift apart. His conclusion carries a note of dark comedy: "It's likely that you would need a consensus algorithm just to generate the fencing tokens." — in which case, why were you using Redlock?

Then the most transferable layer, and the reason the piece is still cited a decade later. The mainstream distributed algorithms — Raft, Paxos, Zab, Viewstamped Replication — make no timing assumptions at all: processes may pause arbitrarily, packets may be arbitrarily delayed, clocks may be arbitrarily wrong. They use clocks only to generate timeouts, and a timeout is a guess, not a verdict.

In plain English, this means that even if the timings in the system are all over the place (processes pausing, networks delaying, clocks jumping forwards and backwards), the performance of an algorithm might go to hell, but the algorithm will never make an incorrect decision.How to do distributed locking, 2016

Redlock is not like that. Its safety itself rests on timing assumptions: that all nodes expire keys after roughly the right duration, that network delay is small relative to the expiry, that process pauses are much shorter than the expiry. In a well-behaved datacenter those hold most of the time — which is exactly the nail he drives in: "If you're depending on your lock for correctness, 'most of the time' is not enough – you need it to always be correct." His verdict is that Redlock is "neither fish nor fowl": unnecessarily heavyweight for efficiency locks, insufficiently safe for correctness ones.

One detail in this piece says more about the man than the argument does. The acknowledgements thank Kyle Kingsbury, Camille Fournier, Flavio Junqueira — and Salvatore Sanfilippo, the author of Redis and of the very algorithm being dismantled. He sent the draft to the person he was criticising, before publishing. The next day Sanfilippo published a rebuttal. Kleppmann neither withdrew the post nor mounted a long defence; he added a short update:

He makes some good points, but I stand by my conclusions. […] but please form your own opinions – and please consult the references below, many of which have received rigorous academic peer review (unlike either of our blog posts).How to do distributed locking, update of 9 February 2016

3. Turn the database inside-out: the log is the truth, the database is its cache

This one starts from something everyone does every day and nobody looks at closely.

You run an UPDATE: customer 123 changes the quantity of product 999 in their cart from 1 to 3. The database finds the row and overwrites 1 with 3. Done. But if you have a follower, the leader also has to ship that change, and one way to do it is to write down the effect the query had — which row changed, and to what.

Kleppmann stopped here, because something had quietly happened. What you wrote was a command: go and modify the rows matching this condition. What comes out in the replication stream is a different kind of thing — an event.

And this is a fact — even if the customer later removes the item from their cart, or changes the quantity again, or goes away and never comes back, that doesn't change the fact that this state change occurred. The fact always remains true.Turning the database inside-out, 2015

In other words: even when you use a database in the wholly traditional way, dutifully overwriting old state with new, the database internally has been translating your commands into a stream of immutable events all along. It is simply hidden behind the public interface and explicitly labelled an implementation detail.

Hold that. He then looks at a second thing: indexes. You write one line of CREATE INDEX and the database scans the table and builds an auxiliary structure. An index adds no new information — it represents existing data in a different shape, which is why dropping it deletes nothing. Better, it is maintained continuously: change the base table and the index follows, often transactionally, so that a rolled-back transaction rolls back the index changes too. PostgreSQL can even build one on a large table while writes continue: the index builder is tracking a moving target, and it catches it.

Third: application-level caching. Which is a mess. Invalidation — when the underlying data changes, how do you know which cache entries to expire? Expiry algorithms that try to work it out are brittle and error-prone; a TTL means accepting stale reads. Race conditions — two processes writing to database and cache may do it in opposite orders. Cold start — reboot the cache and every request is a miss, and the database falls over.

I suspect that most of us building these systems just pretend that the race conditions don't exist, because they are just too much to think about.Turning the database inside-out, 2015

So the contrast sits there: creating a secondary index is one line of SQL, handled automatically, transactionally, online. Maintaining a cache is a pile of invalidation logic, race conditions and operational incidents. Yet mathematically these are the same thing — both are redundant structures derived from the primary data, shaped differently to make reads fast, both rebuildable if lost. So why is one elegant and one a disaster? Not because they differ in difficulty. Because one is the database's responsibility and the other is yours.

The two threads meet, and the proposal follows by itself:

What if we changed our infrastructure so that the replication stream was not an implementation detail, but a key part of the public interface of the database? What if we turn the database inside-out, take the implementation detail that was previously hidden, and make it a top-level concern?Turning the database inside-out, 2015

The payoffs follow. A materialized view is precomputed, so there is no such thing as a cache miss — if it isn't in the view it isn't in the database — and the cold start problem disappears with it. "The log squeezes the non-determinism of concurrency out of the stream of writes": every view built on the same log applies changes in the same order, so they stay consistent with each other, and a whole class of race conditions is gone. Mistakes become recoverable: deploy bad code that writes wrong data and you can look at the log to see exactly what happened and undo it — his analogy is "that's why accountants don't use erasers."

From this he draws the prediction most in need of being held to account: if views are updated from a stream, a client can keep the connection open after reading and be pushed each change, and then request-response is no longer enough — "Basically, I'm saying that in the future, REST is not going to cut the mustard, because it's based on a request-response model." How that prediction has aged is section six.

4. The enemy has changed: it isn't closed source, it's the cloud

April 2021, the Free Software Foundation reinstates Richard Stallman to its board. Kleppmann says he is appalled and joins the call for his removal — "However, this is not what I actually want to talk about today." What he wants to talk about is a re-examination of copyleft, for reasons that have nothing to do with Stallman.

The GPL and other copyleft licenses are not bad; I just think they're pointless.It's time to say goodbye to the GPL, 2021

The shape of the argument is the familiar one: this tool was designed for a different era's enemy. In the 1980s and 90s the enemy of free software was companies selling closed-source software, and the GPL aimed to disrupt that business model. But in the 2020s what takes your computing freedom away is cloud software: Google Docs, Trello, Slack, Figma, Notion — things that run on the vendor's servers with all your data on them.

The problems he lists are hard to argue with. If the company folds or discontinues the product, the software stops working and you are locked out of documents you created. Google may suspend your account with no warning and no recourse, so you could suddenly find yourself permanently locked out of every document you ever created. And the 1990s complaint about not being able to modify closed software is worse in the cloud: with local closed-source software at least someone could reverse-engineer the file format, whereas with cloud software not even that is possible, because the data was never on your disk.

Then the loveliest piece of evidence in the essay. The Internet Archive holds over 100,000 historical software titles that you can still run today in an emulator in your browser — and it never had their source code. For preservation, running the compiled machine code is fine.

What matters isn't openness. It's having a copy at all. Which pulls apart an equation that had been treated as immovable — software freedom equals open source — and yields a conclusion that is genuinely abrasive in open-source circles:

It is nice for local-first software to also be open source, but this is not necessary: 90% of its benefits apply equally to closed-source local-first software.It's time to say goodbye to the GPL, 2021

And the AGPL, designed precisely to close the cloud loophole? He argues it failed empirically: cloud vendors simply refuse to use AGPL-licensed software, and either use a differently-licensed implementation, reimplement it, or buy a commercial license without the copyleft clauses. "I don't think the license has caused any source code to become available that wouldn't have been open source anyway."

His positive programme is the work of his second career: local-first software. In 2019 he and three collaborators at Ink & Switch published the paper of that name at Onward!, subtitled "You Own Your Data, in spite of the Cloud". The definition is plain: the software runs on your own machine and stores its data on your own disk, while retaining what makes cloud software convenient — real-time collaboration and syncing across your devices. The paper sets out seven ideals (headings as in the original):

1. No Spinners: Your Work at Your Fingertips — operations respond to local data instead of waiting for a round trip.
2. Your Work Is Not Trapped on One Device
3. The Network Is Optional — offline is a normal state, not a failure.
4. Seamless Collaboration with Your Colleagues — not "last save wins".
5. The Long Now — you can still open it decades later, long after the company is gone.
6. Security and Privacy by Default
7. You Retain Ultimate Ownership and Control

Under the seventh they take care to disambiguate "ownership" — an act very much in character:

To disambiguate “ownership” in this context: we don't mean it in the legal sense of intellectual property. […] Instead we mean ownership in the sense of user agency, autonomy, and control over data.Local-First Software: You Own Your Data, in spite of the Cloud, 2019

The technical bet is CRDTs. And here the nineteen-year line closes on itself: CRDTs are exactly the kind of thing human reasoning gets wrong. They must converge no matter how messages are reordered, lost or duplicated; the interleavings are too numerous for model checkers to enumerate; and "I think that's probably fine" is the single most dangerous sentence in the vicinity — the sentence he has spent his life taking apart. So he went to Isabelle/HOL, formalising distributed algorithms and doing induction over every possible execution rather than over the cases you thought to test. He is also honest about where the difficulty really sits: the hard part is coming up with an invariant that is both true and strong enough to imply the properties you want, and that step still has to be done by hand.

On 8 December 2025 he made a prediction: LLMs will push formal verification into the mainstream. His arithmetic is candid — the formally verified seL4 microkernel, as of 2009, was 8,700 lines of C, and proving it correct took 20 person-years and 200,000 lines of Isabelle, which is 23 lines of proof and half a person-day for every line of implementation; and the number of people worldwide who can write such proofs he guesses at "maybe a few hundred". In plain economics: for most systems the expected cost of bugs is lower than the expected cost of the proofs that would eliminate them. And he thinks LLMs are unusually well suited to this job, for a very characteristic reason:

It doesn't matter if they hallucinate nonsense, because the proof checker will reject any invalid proof and force the AI agent to retry. The proof checker is a small amount of code that is itself verified, making it virtually impossible to sneak an invalid proof past the checker.Prediction: AI will make formal verification go mainstream, 2025

Stack the four threads and you get one escalating line, each step patching the gap left by the last: first demand more precise words (2015), because wrong words put your confidence in the wrong place; then a better architecture (2015), because some errors shouldn't depend on people being careful; then machine-checked proof (2017–2022), because for the hardest algorithms careful isn't enough; and finally a reason to want any of it (2019–2021), because the technically correct design does not exist if nobody has an incentive to ship it. It started with a German ticket machine.

How he thinks

1. Make it complicated for yourself first, so you can make it simple for everyone else. Hermitage, that test suite spanning four databases, was not a research project. It was background research for one chapter of the book. He says so plainly: "I first had to make it complicated for myself so that I could make it simple (but accurate) for readers." The order can't be reversed: get accurate, then get simple. Starting from simple and reaching for accurate just gets you a very understandable falsehood — like "pick two out of three".

2. Change the representation and the problem often evaporates. This is his oldest and most consistent move, and he had it down long before he touched databases. In 2011, trying to understand company accounts and getting nowhere with accounting books, he found:

Eventually I figured it out: basic accounting is just graph theory. The traditional ways of representing financial information hide that structure astonishingly well, but once I had figured out that it was just a graph, it suddenly all made sense.Accounting for Computer Scientists, 2011

Accounts are nodes, transactions are edges, a balance is the difference between incoming and outgoing edges. A year earlier he had explained valuation caps on convertible notes with graphs, opening the same way. And his 2010 essay "Intuition has no transfer encoding" is very nearly the manual for his later career: intuition is like an enormous bitmap in your head — fast, useful, and impossible to transmit; to get it to someone else you have to vectorise it, choosing a few points and curves carefully. His reason is bracingly practical: so that a team can disagree productively. "By default, intuition comes without a reason attached: you 'simply know' that the answer is X, but you don't know why." DDIA is a vectorisation exercise at scale.

3. When intuition can't say, compute it — even if the answer is alarming. Common wisdom says three replicas are safe: a 0.1% chance per disk means all three failing is one in a billion, less likely than an asteroid. In 2017 he wrote down the binomial distribution and added the variable everyone ignores — how many partitions the cluster has (Cassandra defaults to 256 per node):

Yes, you read that correctly: the risk of losing all three copies of some data is twice as great as the risk of losing a single node! What is the point of all this replication again?The probability of data loss in large clusters, 2017

The intuition fails because it asks whether three particular disks will die together. In an 8,000-node cluster a few nodes are always dead; the real question is whether some partition happens to have all three replicas on dead nodes. More partitions, more chances.

4. Send the draft to the person you're criticising, and mark clearly what you don't know. Almost every technical post ends with an acknowledgements list, and the Redlock one includes the algorithm's author — the person best placed to find the hole in your argument is the person your argument is aimed at. The same disposition shows up in reverse: having finished the data-loss piece, he asks himself "Is this a problem in practice?" and answers "I don't know." The accounting piece ends with "if you spot any mistakes, please let me know"; the convertible-notes disclaimer is blunter: "neither am I a lawyer nor do I have much experience with this stuff, so my explanation may be horribly flawed or simply wrong."

5. Work out whether a thing is worth doing, then publish the ledger. In "Writing a book: is it worth it?" (2020) he itemises the royalties — 108,079 copies, $477,916 — and reports the cost side just as plainly: about 2.5 full-time-equivalent years, one of them with no income at all. The conclusion is that this came out roughly level with what a Silicon Valley engineering salary would have paid over the same period — "But of course I didn't know that at the time! The royalties could easily have turned out to be a factor of 10 lower." Then he runs a more interesting calculation: if only 10% of a hundred thousand readers applied something and each saved a month of wasted engineering, that's 833 engineer-years, over 300x leverage.

How to be a 10x engineer: help ten other engineers be twice as good. Producing high-quality educational materials enables you to be a 300x engineer.Writing a book: is it worth it?, 2020

He doesn't prettify the other side of the ledger either: writing the book was about as hard as building and selling a startup, "that is to say, involving multiple existential crises", and — "The writing process was not good for my mental health." Which probably also explains the shape of the blog: 31 posts in 2008, zero in 2023.

Where he may be wrong

1. His loudest prediction hasn't come true in eleven years. In 2015 he said REST was not going to cut the mustard. In 2026 REST remains the planet's default API style, and "turning the database inside-out" became a real but local architecture inside the Kafka ecosystem rather than anyone's default. And he flagged the gap himself at the time: the most common question people asked was "but what about transactions?", and his answer was "This is a somewhat open research problem." An architecture that has to list transactions as an open research problem is unlikely to go mainstream — he knew that, and didn't let it weaken the conclusion.

2. Seven years on, the cloud is still winning. Google Docs, Notion and Figma have not loosened their grip. His diagnosis is that CRDTs aren't mature enough, which is part of it. But there's a layer he says less about, and I'll mark this as my judgement rather than his: many people stay in the cloud not because of merge algorithms but because they don't have to manage anything — no backups, no device migration, no dead hard drive. "You own your data" quietly hands operational responsibility back to the user, and that responsibility is precisely what the cloud carries for them, and wins them with. None of the seven ideals is "you never have to think about where your data lives again."

3. The GPL piece doesn't meet his own standard. This is the one inconsistency on the site worth singling out. On technical questions he never accepts "I reckon": to check CAP he classified system after system; on data loss he wrote out the binomial; on isolation levels he built a test suite spanning four databases. But arguing that copyleft wasn't important to open source's success, what he offers is: "even in the GPL-licensed projects (e.g. Linux) I am skeptical that the copyleft aspect was really an important factor in the project's success." No data, no counterfactual, no comparison case; the AGPL claim in the same piece has the same shape. This doesn't mean he's wrong — the judgements sound quite reasonable — but it means this piece shouldn't be trusted at the same level as the others, and it happens to be the most political thing on the site. The skill of spotting that gap is one he taught his readers himself.

4. The 2025 prediction is both self-interested and waves away the hardest part. He predicts formal verification is about to go mainstream — and he is himself the person proving distributed algorithms in Isabelle. More importantly, he identifies the real difficulty himself: once verification is automated, the challenge moves to correctly defining the specification, "how do you know that the properties that were proved are actually the properties that you cared about?" That is very nearly the thing formal verification has actually been stuck on for sixty years — not that proofs are expensive, but that specs are hard to get right. His treatment: AI could help translate specifications too, and "there is the potential for subtleties to be lost in translation, but this seems like a manageable risk." By the standard he applied to Redlock, that sentence is a problem. Redlock's flaw was exactly demoting a load-bearing assumption to background noise — "the clocks are probably fine". "The spec will probably translate correctly" is the same sentence.

5. The other side of the Redlock argument was not read for this page. Salvatore Sanfilippo (antirez) published a rebuttal the day after the original, at antirez.com/news/101 (9 February 2016), with a corresponding Hacker News thread. While this page was being written that domain was unreachable from our network environment, so this is reported as a bibliographic fact only; the arguments it makes are not summarised here, because they were not read. What can be confirmed is Kleppmann's own response in the update, and that response is worth seeing: no victory lap — he says the other side makes some good points, that he stands by his conclusions, and then hands judgement to the reader and the references, noting in passing that neither of their blog posts has been peer reviewed.

Sources

• Please stop calling databases CP or APMay 2015. Checks the CAP theorem's definitions word by word, then tries to classify real databases and fails to place a single one. He also wrote a peer-reviewed companion paper, A Critique of the CAP Theorem.
• How to do distributed lockingFebruary 2016. Dismantles Redis's Redlock: locking for efficiency and locking for correctness are different problems; GC pauses and network delays defeat any time-based lock; where fencing tokens come from. The acknowledgements include the algorithm's author.
• Turning the database inside-out with Apache SamzaMarch 2015, an edited transcript of a Strange Loop talk. Four aspects of databases — replication, secondary indexing, caching, materialized views — converging on one conclusion: writes only append to an immutable log, and every database is a view derived from it.
• It's time to say goodbye to the GPLApril 2021. Argues copyleft has become pointless because it targets 1990's enemy; what actually takes your data is the cloud, and the Internet Archive preserved 100,000 programs without ever having their source.
• Local-First Software: You Own Your Data, in spite of the CloudOnward! 2019 paper (PDF, with three co-authors at Ink & Switch). The original source of the seven ideals, and of the case for CRDTs as the technical bet.
• Prediction: AI will make formal verification go mainstreamDecember 2025, the most recent post on the site. The seL4 arithmetic (8,700 lines of C for 20 person-years of proof), and why proof scripts may be one of the best applications for LLMs.

Updates