In the age of LLMs, syntax is no longer the bottleneck for writing, reading, or learning TLA+. People are even getting value by generating TLA+ models and counterexamples directly from Google Docs descriptions of the algorithms. The accidental complexity of TLA+ (its syntax and tooling) is going away.

But the intrinsic complexity remains: knowing where to start a model, what to ignore, and how to choose the right abstractions. This is modeling judgment, and it is the hardest skill to teach. Engineers are trained to think in code, control flow, and local state. TLA+ forces you into a different mode: mathematical, declarative, and global. You specify what must hold, not how to achieve it. Once you get comfortable with this shift, it changes how you think about systems, even away from the keyboard.

In a companion post, I described TLA+ as a design accelerator based on lessons from 8 industry projects. Here I want to go deeper and articulate the mental models behind effective TLA+ use. These are the thinking patterns that TLA+ experts apply implicitly; these are the kind of knowledge acquired by osmosis over the years. I will try to make them explicit and actionable.

The mental models are:

1. Abstraction, abstraction, abstraction
2. Embrace the global shared memory model
3. Refine to local guards and effects (slow is fast)
4. Derive good invariants
5. Explore alternatives through stepwise refinement
6. Aggressively refine atomicity
7. Share your mental models

1. Abstraction, abstraction, abstraction

Abstraction is a powerful tool for avoiding distraction. The etymology of the word abstract comes from Latin for "cut and draw away". With abstraction, you slice out the protocol from a complex system, omit unnecessary details, and simplify a complex system into a useful model. You don't have to model everything. Most of the value comes from knowing what to ignore. The omission is the default: add a component only when leaving it out breaks your reasoning goal.

Abstraction is the art of knowing what to discard. You can cross-cut to focus on the protocol you want to investigate. If you are interested in the consistency model of your distributed system, you can abstract away the mechanics of communication when that is an unnecessary distraction. If you are interested in a replication protocol, you can abstract away the client interaction. Consider two examples from our industry experience.

• CosmosDB consistency modeling: We needed to specify CosmosDB's client-facing consistency semantics. The anti-pattern would have been modeling the distributed database engine, which would have caused an immediate state-space explosion and an unreadable spec. Instead, we modeled just the "history as a log" abstraction for client-facing behavior. The inner details of the database were "environment"; irrelevant to what we were trying to reason about. We used sort-merge to capture the internals of replication, and a read index to model consistency. This way five consistency levels became clear predicates over operation histories.
• Secondary Index at Aurora DSQL: Here, we focused on the secondary index and abstracted away the rest of the database as a log of operations. Log is a common abstraction for State Machine Replication (SMR), which is itself a common abstraction for databases and data stores. By cutting the problem down to its essential slice, we made a complex system tractable.

Leslie Lamport gave a beautiful demonstration of this when he described how he derived Paxos. He started with the most abstract specification: defining agreement based on a vote array. In his words: "I don't remember the thought process that led me to Paxos. But I knew that execution on computers sending messages to one another was an irrelevant detail. I was thinking only about a set of processes and what they needed to know about one another. How they could get that information from messages was the easy part that came later. What I had first was what, many years later, I described as the Voting algorithm."

TLA+ is useful for teaching engineers the art of abstraction and the right way to think and reason about distributed systems. The modeling process itself trains you to ask: what is the behavioral slice I care about, and what can I safely ignore? And because TLA+ gives you a rapid prototyping tool with a tight feedback loop (write a model, check it, revise) you accumulate design experience much faster than you would by building and debugging real systems.

2. Embrace the Global Shared Memory Model

TLA+ gives you a deliberate fiction: a global shared memory that all processes can read and write. This fiction is the foundation of its computational model, and understanding it is essential to thinking in TLA+.

In TLA+, a program consists of two things: (1) a set of variables that define a global state space, and (2) a finite set of actions that transition from one state to the next. This is state-centric reasoning as everything is a predicate (a function mapping to a boolean). This approach promotes invariant-based thinking (see mental model 4).

Each action follows Sir Tony Hoare's triples: {state} action {state'}. The execution of an action is conditional on a predicate (the "guard") being true. For example: x > 0  →  x := 0; y := y + 1. Or in TLA+ notation:

/\ x > 0
/\ x' = 0
/\ y' = y + 1

The guard is a predicate on the state space. If the guard is true in some state, the action is said to be "enabled" in that state. A program begins in any state satisfying the initial predicate. Then an enabled action is nondeterministically selected and executed atomically. This process repeats infinitely. If a selected action's guard is false, it is simply a skip and it does not change the state.

The global shared memory (GSM) model fits naturally with this style of reasoning. You read the current state and install a new state; no channels, no message serialization, no process boundaries to manage. It is the most minimal way to write models that fit the guarded-command model. Be frugal in defining variables, though: each one exponentially explodes the state space. The payoff is that safety and liveness become compact predicates over global state. Your program defines an invariant set (i.e., the good states) and must never transition out of it.

You don't have to model channels, message serialization, or network topology unless those are the specific things you're reasoning about. It is possible to map GSM to message passing if you keep to "localish" guards and definitely local variable assignments. What do we mean by "local variable" in a global shared state space? A common way is to use indices per node, so vote[i] refers to node i's vote. The global variable is the vote array, and the local version is vote[i]. It's all math, and math needs abstraction. TLA+'s computational model that is shaped around the global shared memory fiction enables you reason at the right level of abstraction.

3. Refine to local guards and effects (slow is fast)

The global shared memory fiction of TLA+ is powerful for reasoning, but it creates a trap: it is easy to write guards that read global state no real process could observe atomically. This is one of the most common modeling errors. A guard that checks what three different nodes have done simultaneously is "illegal knowledge" as no single node in a real distributed system can know all of that at once. A dedicated review pass should ask, for every action: what information could a real node actually know when it decides to act?

So how do you transform your guards to be local? There is a folk theorem that reading your immediate neighbor is fine because it can be mapped to message passing (think hygenic dining philosophers). This essentially boils down to adding another level of indirection and proxy variables, which means locking. Locking is not good for performance, and in mental model 6 I will advocate that you should refine your atomicity and allow as much concurrency as possible for the implementation to enjoy freedom responsibly. So what do we do?

The key insight is to try to figure out stable, monotonic, or locally stable predicates to use for your guards. In my "Hints for Distributed Systems Design", when I tell you to "embrace monotonicity", I am thinking of exactly this: "For doing coordination efficiently and safely in a distributed system, the insight is almost always to transform the problem into a monotonic one."

This is where things get subtle, and it touches on esoteric knowledge that is rarely made explicit. This is something you get to intuit after years of working on distributed systems close to the theoretical side. Your advisor intuited it, their advisor intuited it, they had developed vocabulary shortcuts to refer to this but never made it fully explicit. UC Berkeley's efforts on CALM (Consistency As Logical Monotonicity) made this more concrete by basing it on a language like Dedalus, but the basic gist lives at the level of abstract global state reasoning.

In our "Slow is Fast" paper, we formalized this intuition by partitioning actions into "slow" and "fast". A slow action's guard remains true even if the node's information is slightly stale. This is because either the guard is a stable predicate (once true, stays true), depends only on local variables, or is a locally stable predicate (only the node's own actions can falsify it). A fast action, by contrast, requires fresh global state to evaluate its guard. The key result is this: if you can make your guards locally stable, the protocol requires less coordination and tolerates communication delays gracefully. Hence, slow is fast.

This is not easy to do. Ernie Cohen had internalized this skill, and he could quickly zero in on the monotonic or locally stable predicates to exploit in his protocol explorations. Some people live in this way of thinking so completely that they may not even know how to articulate it, like fish in water. (Case in point: the phrase "global shared memory fiction" was pointed out to me by Marc Brooker. Sometimes it takes a slight outsider to name what insiders take for granted.) The practical takeaway for TLA+ modeling is this: when you write your guards, ask yourself whether the information the guard relies on could become stale, and if so, whether the guard is still safe to act on. If you can make your guards depend on monotonic or locally stable predicates, your protocol will be more robust, more concurrent, and closer to a correct distributed implementation.

Lamport’s derivation of Paxos illustrates this beautifully. He begins with the simplest specification of consensus: chosen starts as the empty set and transitions to a singleton {v}. That is the entire next-state formula. He then refines to a voting algorithm where acceptors vote and a value is chosen if a majority votes for it, and refines further to Paxos to handle the problems that arise (what if N acceptors vote for v1, N for v2, and the remaining acceptor fails?). At each refinement step, the guards become more local. In Paxos, the guard for whether an acceptor should cast a vote depends on local knowledge: what ballots this acceptor has participated in. The monotonic structure of ballot numbers ensures that this local knowledge does not become invalid: once an acceptor knows something about the progress of voting, that fact is permanent. This is what makes Paxos work despite asynchrony and failures.

4. Derive good invariants

You did the modeling for a purpose, not for sport. You want to arrive at reasoning insights about your protocol, and invariants are the distilled version of those insights. Invariant-based reasoning is non-operational: instead of tracing execution paths and happy-path thinking, you ask "what needs to go right?" You specify the boundary conditions, and the model checker explores all possible interleavings to verify them.

Spend time distilling good invariants because they serve you in many ways. They guide you as you explore protocol variants (see mental model 5), telling you what you can and cannot change. They act as contracts when you compose components, defining what each part guarantees to the others. They translate directly into runtime assertions and test oracles for your implementation. And they are essential for adding fault-tolerance: once you know the invariant, you know where you need to recover to after a fault, and you can design recovery actions to reestablish it.

Invariant writing is still mostly manual. LLMs struggle with it because invariants are the most signal-heavy part of a spec: they distill your understanding of what this protocol must guarantee. Getting them right means you have closure on the problem.

People new to TLA+ and formal methods repeatedly fail at this step. I occasionally struggle with it too, especially when entering an unfamiliar domain I have to first pay my dues and think harder to gain understanding. The most common failure mode is writing "trivial invariants" that are always true regardless of what the protocol does; you've written the spec for naught. Another is confusing the "end state" with an invariant: an invariant must hold at every reachable state, not just the final one. We are not expecting inductive invariants (that is harder still, and more valuable since a formal proof follows easily from one). But a reasonably tight invariant that demonstrates understanding and scaffolds further exploration, and that is what you should aim for.

Don't stop at safety properties (what the system is allowed to do). Write liveness properties too (what the system must eventually do). It is important to check properties like <> Termination and Init ~> Solution. Do requests complete? Do leaders emerge? Many "correct" models quietly do nothing forever. A model that never violates safety but makes no progress is useless. Checking liveness catches paths that stall, specs that are overly constrained, and actions that never get enabled.

Returning to our running example: in Lamport's Paxos derivation, the invariants at each refinement level are instructive. At the Consensus level, the safety invariant is simply that at most one value is chosen (Cardinality(chosen) <= 1). At the Voting level, chosen is defined as the set of values for which there exists a ballot where a quorum of acceptors all voted for that value (chosen == {v \in Value : \E b \in Ballot : ChosenAt(b, v)}). The safety of the Voting algorithm rests on two rules: (1) different acceptors cannot vote for different values in the same ballot, and (2) an acceptor may only vote for value v in ballot b if v is safe at b. These invariants are tight, non-trivial, and they scaffold the entire refinement chain down to Paxos. They show genuine understanding of why consensus works, and that is what I mean by "closure on the problem".

5. Explore alternatives through stepwise refinement

One of TLA+'s greatest strengths is that it supports fast exploration of protocol variants. The key technique is stepwise refinement: start with the most abstract specification of your problem, then progressively add implementation detail, verifying at each step that the refinement preserves the invariants from the level above.

The canonical example is again Lamport's derivation of Paxos. The abstract Consensus spec defines a single variable chosen that transitions from the empty set to a singleton. Then an intermediate Voting model is defined and shown to be a refinement of Consensus. It describes what properties voting must satisfy, but not how acceptors implement them. Finally, the Paxos model refines Voting by adding message passing, ballot leaders, and the two-phase protocol. At each level, the refinement adds detail (ballots, quorums, messages) while preserving the safety property from above.

Refinement is at the heart of abstraction and a cornerstone of TLA+. In TLA+, refinement is simply implication: the concrete system's behaviors must be a subset of the abstract system's allowed behaviors. You check this by declaring an instance of the abstract spec in the concrete one and verifying via TLC that every behavior of the concrete system is an accepted behavior of the abstract system. Even invariant checking is refinement in disguise: does the system model implement this invariant formula?

A big advantage of stepwise refinement is that when you want to explore a protocol variant, you don't start from scratch. You go back up to the appropriate level of abstraction, change one refinement step, and get a different protocol that still satisfies the same high-level specification. This is systematic design space exploration. With LeaseGuard, for example, we started modeling a lease protocol for Raft early. While refining the abstract spec, we discovered two optimizations we hadn't anticipated, including inherited lease reads, which we probably wouldn't have found without thinking at multiple levels of abstraction.

A common failure pattern here is getting stuck at a level of detail, patching corner cases one by one. This is the implementation mindset leaking into modeling. When this happens, go back up. I saw this with the Secondary Index project at Aurora DSQL: an engineer's design was growing by accretion, each corner-case patch creating new corner cases. TLA+ forced a different approach: specify what the secondary index must guarantee abstractly, then search the solution space through refinement. Over a weekend, with no prior TLA+ experience, the engineer had written several variations. The lesson: specify behavior, not implementation, then explore different "how" choices through refinement.

6. Aggressively refine atomicity

Overly large atomic actions hide races. If your TLA+ action does ten things atomically in a single step, you're sweeping concurrency under the rug. The model will look correct, but it won't represent the interleavings your real system will face. Actions should be as fine-grained as correctness allows. Smaller steps expose the interleavings the protocol must tolerate and make invariants more meaningful.

A practical approach is to start coarse-grained to establish correctness, then systematically split actions into smaller steps and verify safety still holds. This is stepwise refinement (mental model 5) applied to action granularity. Each split increases the interleaving space, which is precisely where TLC earns its keep: the interference surface area may explode, but TLC will exhaustively check that your invariants hold.

The goal here is to give the implementation maximum freedom to reorder and parallelize, while verifying that the protocol remains correct under that concurrency. Fine-grained atomicity in the spec means the implementation can schedule operations in any order that respects the guard conditions.

Our StableEmptySet project is a good example. Ernie Cohen pushed atomic actions to the finest possible granularity to avoid distributed locking, and the resulting protocol was more concurrent than a lock-based design. The interleaving surface area increased, but TLC handled it without breaking a sweat. This is where the "slow is fast" insight (mental model 3) connects back: by refining guards to depend on locally stable predicates, you can split actions finely without introducing illegal knowledge: the guards remain valid even as the global state changes between steps.

7. Share your mental models

TLA+ models are also meant to be communication tools. A well-written spec serves as precise, executable documentation of a protocol, capturing design intent in a way that prose specifications and code comments cannot match.

At AWS, when I wrote the first TLA+ model of Aurora DSQL's distributed transaction protocol, the model's value quickly went beyond correctness confidence. It served as a communication anchor for a large team. When we sought further formal methods support, the TLA+ models sped up onboarding for new team members and kept everyone aligned on the protocol's design. Instead of arguing over ambiguous prose in a design document, the team could point to specific actions and invariants in the spec.

Our MongoDB distributed transactions work reinforces this. We wrote the first modular TLA+ specification of the protocol many years after it was in production. The model now serves as an authoritative description of what the protocol actually guarantees, bringing clarity to a system that had become difficult to reason about as a whole.

So, you should write your specs for humans, not just for TLC. Use clear action names, write TypeOK invariants early (they serve as executable documentation of your data model), and make every important property an explicit invariant. A well-structured spec communicates protocol intent more clearly than thousands of lines of implementation code, because it shows the essential logic without the noise of error handling, serialization, and configuration.

Tools like Spectacle can visualize TLA+ state spaces and execution traces, bridging the gap between mathematical precision and the operational intuition engineers thrive on. TLA+ is one of the purest intellectual pleasures: reducing a complex distributed system to its essential logic. Please share that pleasure with others by writing about your models, presenting them, and using them to teach.

As LLMs write more of our code, the value of TLA+ for design and reasoning will only grow. TLA+ has the potential to become a cornerstone in an AI+formal methods stack for building systems. The mental models I've described here are the foundation for that future. By mastering abstraction, embracing the global shared memory model, refining to local guards, deriving good invariants, exploring alternatives through refinement, aggressively refining atomicity, and sharing our mental models, we can unlock the full power of TLA+ to design better distributed systems in the age of AI. 

CedarDB: Catching Up on Recent Releases

This post takes a closer look at some of the most impactful features we have shipped in CedarDB across our recent releases. Whether you have been following along closely or are just catching up, here is a deeper look at the additions we are most excited about.

Parquet support: Your On-Ramp to CedarDB

v2026-03-03

Due to the significant compression facilitated by its columnar format, Parquet has become quite popular in the past several years. Today we find Parquet in projects like Spark, DuckDB, Apache Iceberg, ClickHouse, and others. Because of this, Parquet has become not only a data format for running analytical queries, but also a handy format for data exchange between OLAP engines. CedarDB is now able to read Parquet data and directly load it into its own native data format with a single SQL statement:

postgres=# select * from 'data.parquet' limit 6;
 id | name | email | age | city | created_at
----+---------------+-------------------+-----+-------------+------------
 1 | Alice Johnson | alice@example.com | 29 | New York | 2024-01-15
 2 | Bob Smith | bob@example.com | 34 | Los Angeles | 2024-02-20
 3 | Clara Davis | clara@example.com | 27 | Chicago | 2024-03-05
 4 | David Lee | david@example.com | 41 | Houston | 2024-04-18
 5 | Eva Martinez | eva@example.com | 23 | Phoenix | 2024-05-30
 6 | Frank Wilson | frank@example.com | 38 | San Antonio | 2024-06-12
(6 rows)

CREATE TABLE my_table as SELECT * from 'data.parquet';

This makes migrating from other OLAP systems, or ingesting data from your data lake, straightforward. Check out our Parquet Documentation and our hands-on comparison of CedarDB vs. ClickHouse using StackOverflow data, where CedarDB was 1.5-11x faster than ClickHouse after a Parquet-based migration.

Better Compression, Less Storage: Floats and Text

v2026-01-22 and v2025-12-10

Storage efficiency has seen a major leap on two fronts. For floating-point columns (i.e., of type REAL and DOUBLE PRECISION ), CedarDB now applies Adaptive Lossless Floating-Point compression (ALP), a state-of-the-art technique that halves the on-disk footprint (on average) - perfect for workloads heavy on sensor readings or metrics.

For TEXT columns, we’ve adopted FSST (Fast Static Symbol Tables) combined with dictionary encoding: in practice this can halve the storage size of text-heavy tables while also making queries faster, since less data needs to be read from disk. Read our deep-dive blog post on the FSST implementation here.

without DictFSST:

postgres=# SELECT 100 * ROUND(SUM(compressedSize)::float / SUM(uncompressedSize), 4) || '%' as of_original FROM cedardb_compression_info WHERE tableName = 'hits' AND attributeName = 'title';
 of_original
-------------
 21.83%
(1 row)

with DictFSST:

postgres=# SELECT 100 * ROUND(SUM(compressedSize)::float / SUM(uncompressedSize), 4) || '%' as of_original FROM cedardb_compression_info WHERE tableName = 'hits' AND attributeName = 'title';
 of_original
-------------
 13.42%
(1 row)

Improve Parallelism of DDL and Large Writes

v2026-02-03

Schema changes and parallel bulk loads no longer bring your database to a halt. CedarDB now supports DDL operations like ALTER TABLE and CREATE INDEX on different tables in parallel. Similarly, large INSERT , UPDATE and DELETE operations now also run in parallel. None of these operations impact parallel readers anymore. For teams running mixed OLTP/OLAP workloads, this is a significant quality-of-life improvement.

PostgreSQL Advisory Locks

v2025-11-06

CedarDB now has full support for PostgreSQL advisory locks, including blocking variants that wait until a resource is freed and automatic deadlock detection. This fills an important compatibility gap for operational applications that use advisory locks for custom mutual exclusion either to implement custom functionality (think job schedulers or distributed task queues) or require them for correctness guarantees (think schema migration tools). Check out our advisory locks documentation for more info.

SELECT pg_advisory_lock(123);
-- ... do work ...
SELECT pg_advisory_unlock(123);

Late Materialization

v2026-01-15

Internally, CedarDB now delays fetching column data until it’s actually needed, a technique called late materialization. When a query filters out most rows early, this means only the surviving rows ever have their full column data fetched from storage. The result is faster queries on wide tables, with less wasted I/O. This improvement is transparent: no changes required to your queries or schema.

In the example below, a table scan is reduced from reading 24 GB on disk to just 75 MB.

Before:

postgres=# explain analyze SELECT * FROM hits WHERE url LIKE '%google%' ORDER BY eventtime LIMIT 10;
 plan 
-------------------------------------------------------------------------------------------------------------------------------------------------------------------------
 🖩 OUTPUT () +
 ▲ SORT (In-Memory) (Result Materialized: 626 KB, Result Utilization: 83 %, Peak Materialized: 635 KB, Peak Utilization: 83 %, Card: 10, Estimate: 10, Time: 0 ms (0 %))+
 🗐 TABLESCAN on hits (num IOs: 29'046, Fetched: 24 GB, Card: 853, Estimate: 67'688, Time: 10632 ms (100 % ***))
(1 row)

Time: 10651.826 ms (00:10.652)

After:

postgres=# explain analyze SELECT * FROM hits WHERE url LIKE '%google%' ORDER BY eventtime LIMIT 10;
 plan 
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
 🖩 OUTPUT () +
 l LATEMATERIALIZATION (Card: 10, Estimate: 10) +
 ├───▲ SORT (In-Memory) (Result Materialized: 29 KB, Result Utilization: 58 %, Peak Materialized: 34 KB, Peak Utilization: 60 %, Card: 10, Estimate: 10, Time: 10 ms (8 % *))+
 │ 🗐 TABLESCAN on hits (num IOs: 20, Fetched: 75 MB, Card: 482, Estimate: 67'688, Time: 116 ms (92 % ***)) +
 └───🗐 TABLESCAN on hits (Estimate: 10)
(1 row)

Time: 139.806 ms

New Types: Unsigned Integers, UUIDv7, and Enums

v2025-11-06, v2025-10-22, and v2026-01-22

Three type additions make CedarDB more expressive:

• Unsigned integers (UINT1 - UINT8): Useful for importing data from Parquet, which also has native unsigned types. Also the right fit for any domain where negative values are nonsensical (counts, IDs, IP ports, flags). No more workaround with larger signed types!
• UUIDv7: A newcomer from Postgres 18. Unlike UUIDv4, UUIDv7 embeds a timestamp and is monotonically increasing, making it index-friendly and suitable as a primary key without the index fragmentation problems of random UUIDs. Check out our UUID Documentation for more info.
• Enum types: Columns can now be declared with a fixed set of string values, saving storage and making constraints explicit at the type level. Check out our Enum Documentation for more info.

CREATE TYPE order_status AS ENUM ('pending', 'processing', 'shipped', 'delivered', 'cancelled');

CREATE TABLE orders (
 id UUID PRIMARY KEY DEFAULT uuidv7(),
 status order_status NOT NULL DEFAULT 'pending',
 quantity UINT4 NOT NULL,
 total_cents UINT4 NOT NULL
);

INSERT INTO orders (status, quantity, total_cents) VALUES ('pending', 2, 1999), ('processing', 1, 4999), ('shipped', 5, 2495);

postgres=# select * from orders;
 id | status | quantity | total_cents 
--------------------------------------+------------+----------+-------------
 019d0701-cb64-7c96-b90c-ebd4a4410dee | pending | 2 | 1999
 019d0701-cb65-7c49-8a1a-2e4ea96a85b1 | processing | 1 | 4999
 019d0701-cb65-74ce-a987-b72905eb7f7a | shipped | 5 | 2495
(3 rows)

PostgreSQL Compatibility: Moving Fast

CedarDB’s PostgreSQL compatibility continues to expand rapidly. Recent months have brought new SQL grammar support, a growing roster of system functions and un-stubbed catalog tables, and bug-for-bug compatibility fixes that allow more existing PostgreSQL tooling to work out of the box.

If a tool or library failed to connect or misbehaved in a previous version, it’s worth trying again - the list of working clients and frameworks is growing steadily. If your favorite tool isn’t working yet, please let us know by creating an issue.

That’s it for now

Questions or feedback? Join us on Slack or reach out directly.

Do you want to try CedarDB straight away? Sign up for our free Enterprise Trial below. No credit card required.

As I mentioned in my previous blog post, I recently got my hands on Claude Code. In the morning, I used it to build a Hybrid Logical Clocks (HLC) visualizer. That evening, I couldn't pull myself away and decided to model something more ambitious. 

I prompted Claude Code to design a Paxos tutorial game, BeatPaxos, where the player tries to "beat" the Paxos algorithm by killing one node at a time and slowing nodes down. Spoiler alert: you cannot violate Paxos safety (agreement). The best you can do is delay the decision by inducing a series of well-timed failures, and that is how you increase your score.

MariaDB 12.3 has a new feature enabled by the option binlog_storage_engine. When enabled it uses InnoDB instead of raw files to store the binlog. A big benefit from this is reducing the number of fsync calls per commit from 2 to 1 because it reduces the number of resource managers from 2 (binlog, InnoDB) to 1 (InnoDB).

My previous post had results for sysbench with a small server. This post has results for the Insert Benchmark with a large (32-core) server. Both servers use an SSD that has has high fsync latency. This is probably a best-case comparison for the feature. If you really care, then get enterprise SSDs with power loss protection. But you might encounter high fsync latency on public cloud servers.

While throughput improves with the InnoDB doublewrite buffer disabled, I am not suggesting people do that for production workloads without understanding the risks it creates.

tl;dr for a CPU-bound workload

• throughput for write-heavy steps is larger with the InnoDB doublewrite buffer disabled
• throughput for write-heavy steps is much larger with the binlog storage engine enabled
• throughput for write-heavy steps is largest with both the binlog storage engine enabled and the InnoDB doublewrite buffer disabled. In this case it was up to 8.9X larger.

This is an external post of mine. Click here if you are not redirected.

MariaDB 12.3 has a new feature enabled by the option binlog_storage_engine. When enabled it uses InnoDB instead of raw files to store the binlog. A big benefit from this is reducing the number of fsync calls per commit from 2 to 1 because it reduces the number of resource managers from 2 (binlog, InnoDB) to 1 (InnoDB). See this blog post for more details on the new feature.

My previous post had results for sysbench with a small server. This post has results for the Insert Benchmark with a large (48-core) server. Storage on this server has a low fsync latency while the small server has high fsync latency.

tl;dr

• binlog storage engine makes some things better without making other things worse
• binlog storage engine doesn't make all write-heavy steps faster because the commit path isn't the bottleneck in all cases on a server with storage that has low fsync latency

tl;dr for a CPU-bound workload

• the l.i0 step (load in PK order) is ~1.3X faster with binlog storage engine
• the l.i2 step (write-only with smaller transactions) is ~1.5X faster with binlog storage engine

Yesterday morning I downloaded Claude Code, and wanted to see what this bad boy can do. What better way to learn how this works than coding up a toy example with it. The first thing that occurred to me was to build a visualizer for Hybrid Logical Clocks (HLC).

HLC is a simple idea we proposed in 2014: combine physical time with a logical counter to get timestamps that are close to real time but still safe under clock skew. With HLC, you get the best of both worlds: real-time affinity augmented with causality when you need it. Since then HLC has been adopted by many distributed databases, including MongoDB, CockroachDB, Amazon Aurora DSQL, YugabyteDB, etc.

This felt well scoped for a first project with Claude Code. Choosing Javascript enabled me to host this on Github (Git Pages) for free. Easy peezy way of sharing something small yet useful with people. 

Claude Code is a clever idea. It is essentially an agent wrapped around the Claude LLM. Chat works well for general Q/A, but it falls short for coding. In Claude Code, the agent wraps the LLM with a UNIX terminal abstraction, and voila, we are set up for coding. Simple and effective. It is the right interface. The terminal reduces everything to small modular, composable commands. Terminal commands were the original microservices! You compose these well-defined tools with pipes to build larger workflows. Everything is text, which plays to the strengths of LLMs. Add git for versioning, and you get a tight development loop.

The process went smoothly (very smoothly, in fact) despite this being my first time using Claude Code. I described Claude what I wanted to build. Since this was my first time, I gave a very brief description, I didn't expect it to jump to action based on this minimal description. (More on this at the end of the post.)

Claude created the hlc-visualizer directory, produced the first version of index.html, and opened it in Chrome to show me the demo. I was impressed by the speed. Wow. It almost got there on the first shot. The liberties it took with the layout were smart. It used a vertical time diagram and three nodes at the top. Both made it to the final version.

The initial visualization used buttons for send and local events. These sat on the right pane, away from the action, and were not easy to use. I prompted Claude to switch to double click on a node timeline for local events, and drag and drop between timelines for send events. This felt more natural, but I was not sure Claude could pull it off. It did, on the first try.

For the record, I used Sonnet. Since this was my first experiment with Claude, I did not want to use Opus, the more expensive model. Maybe Opus would have produced a better first version. I do not know.

Agents do not seem good with timing. The simulation ran too fast for human interaction. I kept tuning it to a tolerable speed. The screen also did not follow the timeline as new events extended beyond the view. See the commit log for how this evolved. I was not very efficient because this was my first time using Claude.

I think my biggest contribution to this collaboration was to notice that we need a snapshot feature. That's the killer app for HLC. So I explained Claude how snapshot should be taken, and after a couple of iterations, that worked. After that, I focused on improving the interaction and visuals.

Here is the end product. Try it here. Feedback is welcome in comments. 

All in all, this was delightful. I wish I had this when I was teaching. It would help create visualizations for algorithms quickly. Students need hands-on interactive learning, not static figures. They need to play with the algorithms, explore corner cases, and see how the algorithms behave. I used TLA+ for teaching my distributed systems class, but visualizations like this are the real deal. I will do my usual plug for Spectacle, browser based TLA+ trace explorer and visualizer. But even with the manual animation mode, I think it will hard to code this time diagram visual and snapshots there.

A final note on personality. Claude has high energy. It is a go-getter. It skips small talk, like a seasoned developer. It does not ramble like ChatGPT. Gemini Pro comes across as sound, but it sounds too uptight and uncreative when writing prose. Claude Code feels smart and sharp when coding.

This chapter from Operating Systems: Three Easy Pieces explores multiprocessor scheduling as we transition from the simpler world of single-CPU systems to the challenges of modern multicore architectures.

This is part of our series going through OSTEP book chapters. The OSTEP textbook is freely available at Remzi's website if you like to follow along.

Core Challenges in Multiprocessor Scheduling

The shift to multiple CPUs introduces several hardware challenges that the operating system must manage:

• Cache Coherence: Hardware caches improve performance by storing frequently used data. In multiprocessor systems, if one CPU modifies data in its local cache without updating main memory immediately, other CPUs may read "stale" (incorrect) data.
• Synchronization: Accessing shared data structures across multiple CPUs requires mutual exclusion (e.g., locks). Without these, concurrent operations can lead to data corruption, such as double frees in a linked list.
• Cache Affinity: Processes run faster when they stay on the same CPU because they can reuse state already built up in that CPU's local cache. Frequent migration across CPUs forces the system to reload this state, degrading performance.

Yep. Now we are talking about some distributed systems concepts, even inside a single computer.

Scheduling Strategies

The chapter compares two primary architectural approaches to scheduling:

1. Single-Queue Multiprocessor Scheduling (SQMS): All jobs are placed into a single global queue. This is simple to implement and inherently balances the load across all available CPUs, but it does not scale well due to lock contention on the single queue and often ignores cache affinity.
2. Multi-Queue Multiprocessor Scheduling (MQMS): The system maintains multiple queues, typically one per CPU. This is highly scalable and naturally preserves cache affinity since jobs stay in their assigned queue, but is vulnerable to load imbalance, where one CPU may become idle while another is overloaded.

To address load imbalances in MQMS, systems use "work stealing", where an under-utilized CPU peeks at another queue and steals jobs to balance the workload.

Modern Linux schedulers have utilized both approaches:

• O(1) Scheduler: Multi-queue.
• Completely Fair Scheduler (CFS): Multi-queue.
• BF Scheduler (BFS): Single-queue.

When you are in TPOT echo chamber, you would think fully autonomous AI agents are running the world. But this 2025 December paper, "Measuring Agents in Production" (MAP), cuts through the reality behind the hype. It surveys 306 practitioners and conducts 20 in-depth case studies across 26 domains to document what is actually running in live environments. The reality is far more basic, constrained, and human-dependent than TPOT suggest.

The Most Surprising Findings

Simplicity and Bounded Autonomy: 80% of case studies use predefined structured workflows rather than open-ended autonomous planning, and 68% execute fewer than 10 steps before requiring human intervention. Frankly, these systems sound to me less "autonomous agent" than glorified state machine or multi-step RAG pipeline. 

Prompting Beats Fine-Tuning: Despite the academic obsession with reinforcement learning and fine-tuning, 70% of teams building production agents simply prompt off-the-shelf proprietary models. Custom-tuned models are often too brittle, and they break when foundation model providers update their models.

Tolerance for Latency: While in database systems and distributed systems we focus on shaving milliseconds and microseconds off response times, in the agent world 66% of deployed systems take minutes or even longer to respond. I am not comparing or criticizing because of the intrinsically different nature of the work, I am just stating how vastly different the latency expectations are.

Custom Infrastructure Over Heavy Frameworks: Though many developers experiment with frameworks like LangChain, 85% of the detailed production case studies ended up building their systems completely in-house using direct API calls. Teams actively migrate away from heavy frameworks to reduce dependency bloat and maintain the flexibility to integrate with their own proprietary enterprise infrastructure.

Benchmarks are Abandoned: 75% of production teams skip formal benchmarking entirely. Because real-world tasks are incredibly messy and domain-specific, teams rely instead on A/B testing, production monitoring, and human-in-the-loop evaluation (which a massive 74% of systems use as their primary check for correctness).

Reliability (consistent correct behavior over time) remains the primary bottleneck and challenge. OK, this one was not really a surprising finding. 

Discussion

So the data says that the state of multi-agent systems in production is exaggerated. Everyone says they are doing it, but only a few actually are. And those who are doing it are keeping it basic.

This feels familiar.

Remember 2018? IBM published a whitepaper stating that "7 in 10 consumer industry executives expect to have a blockchain production network in 3 years". They famously claimed blockchains would cure almost every business ailment, reducing 9 distinct frictions including "inaccessible marketplaces", "restrictive regulations", "institutional inertia", "invisible threats", and "imperfect information". Ha, "invisible threats", it cracks me up every time!

But, comparing AI agents to blockchains is unfair. Agents actually have a couple killer applications already. They have also made it into deployment despite in very basic and constrained manner. It's just that they aren't the fully autonomous hyper-intelligent multi-agent swarms that people claim they are. They remain basic, human-supervised, highly constrained tools.

I started to use TPROC-C from HammerDB to test MariaDB, MySQL and Postgres and published results for MySQL and Postgres on small and large servers. This post provides more detail on CPU overheads for MariaDB, MySQL and Postgres on a small server.

tl;dr

• Postgres get the most throughput and the difference is large.
• MariaDB gets more throughput than MySQL
• Throughput improves for MariaDB and MySQL but not for Postgres when stored procedures are enabled. It is possible that the stored procedure support in MariaDB and MySQL is more CPU efficient than in Postgres.
• Postgres uses ~2X to ~4X more CPU for background tasks than InnoDB. The largest contributor is (auto)vacuum. But the total amount of CPU for background tasks is not significant relative to other CPU consumers.

Retry storms are infamous in distributed systems. It is easy to run into them. Inevitably, a downstream service experiences a hiccup, so your clients automatically retry their failed requests. Those retries add more load to the struggling service, causing more failures, which trigger more retries. Before you know it, the tiny unavailability cascades into a full-blown self-inflicted denial of service.

Token Bucket is a popular technique that helps with gracefully avoiding retry storms. Here is how the token bucket algorithm works for retries:

• Sending is always free. When a client sends a brand-new request, it doesn't need a token. It just sends it.
• Successes give you credit. Every time a request succeeds, the client deposits a small fraction of a token into its bucket (up to a maximum capacity).
• Retries costs you credit. If a request fails, the client must spend a whole token (or a large fraction of one) to attempt a retry.

If the downstream service is healthy, the bucket stays full. But if the service goes down, the initial failures quickly drain the bucket. Once the bucket is empty, the client stops retrying. It gracefully degrades, protecting the downstream service until it recovers and new requests start succeeding again.

It is an elegant solution. But when implementing it in a client driver, there is a subtle concurrency trap that is easy to fall into. We model it below to show exactly where things go wrong.

The Sequential Processing Trap

When an engineer sits down to write a client driver, they usually think sequentially: Pull a request from a queue, send it, check the response, and retry if it fails. We can model this sequential control flow using PlusCal (the pseudoalgorithm DSL that compiles down to TLA+). In this first model below, we simulate a thread iterating over a queue of requests. If a request fails, the thread checks the token bucket. If the bucket is empty, the thread naturally awaits for tokens to become available.

(Aside:  Before we look at the results, notice the placement of labels in the model. In PlusCal, labels are not just aesthetic markers or simple goto targets. They are structurally vital because they define the boundaries of atomic steps. Label to label is the unit of atomic execution, so we have to place them very deliberately. For example, making a request to a server and evaluating its response cannot be a single, instantaneous action. It violates the physical reality of the network boundary. By placing the ProcessResponse: label right before the if server_succeeds check, we correctly split this into two atomic actions. As a fun piece of TLA+ trivia: if we omitted that label, the model checker would evaluate the network call and the await statement simultaneously. To avoid getting stuck at an invalid await state, TLC would magically "time travel" and force the server to succeed every single time, completely hiding our bug! )

If we run this model, the TLC model checker immediately throws a Termination violation. Why?

We accidentally built a Head-of-Line (HOL) blocking bug. This is how it happens. A burst of failures drains the bucket. The thread hits the "await condition" and goes to sleep, waiting for tokens. But because the thread is blocked, it can't loop around to send new requests. Since only new requests can earn tokens, the bucket will never refill, and the client driver is permanently deadlocked.

The Fix: Fail-Fast

To fix this, we have to change how the client driver reacts to an empty bucket. Instead of waiting, it must fail-fast. So we remove the "await" and simply drop the request if we can't afford the retry. We unblock the queue as the thread moves on to the next request. TLC confirms that this model passes with flying colors. starvation, no deadlocks.

The Pure TLA+ Perspective

It is worth noting that if we had modeled this system using pure TLA+ from the start, we wouldn't have stumbled into this specific deadlock. Instead of sequential thread logic, Pure TLA+ models state machines and event-driven logic. In the below TLA+ model, Send, ServerRespond, Retry, and Drop are independent actions. If the bucket is empty, the Retry action simply becomes disabled. But because there is no while loop tying actions together, the Send action remains perfectly valid for any new incoming requests. The guarded-command TLA+ model below naturally avoids the head-of-line blocking problem.

To run this TLA+ model at Spectacle web tool for visualization, simply click this link. The Spectacle tool loads the TLA+ spec from GitHub, interprets it using JavaScript interpreter, and visualizes step-by-step state changes as you press a button corresponding to an enabled action. You can step backwards and forwards, and explore different executions. This makes model outputs accessible to engineers unfamiliar with TLA+. You can share a trace simply by sending a URL as I did above.

This brings us to an important lesson about formal verification and system design: the paradigm gap. Pure TLA+ is a beautiful event-driven way to describe the mathematically correct state of your system. However, the environments where these systems actually live (Java, Go, C++, or Rust) are fundamentally built around sequential threads, loops, and queues, just like our PlusCal model. The impedance mismatch between an event-driven specification and a sequential implementation introduces the risk of HOL blocking. Because modern programming languages make it so effortless to pause a thread and wait for a resource, it is incredibly easy for a system to fall into the blocking trap. We should be cognizant of this pitfall when implementing our designs. 

This paper proposes a way to get serializability without completely destroying your system's performance. I quite like the paper, as it flips the script on how we think about database isolation levels. 

The Idea

In modern hardware setups (where we have massive multi-core processors, huge main memory, and I/O is no longer the main bottleneck), strict concurrency control schemes like Two-Phase Locking (2PL) choke the system due to contention on centralized structures. To keep things fast, most systems default to weaker schemes like Snapshot Isolation (SI) or Read Committed (RC) at the cost of allowing dependency cycles and data anomalies. Specifically, RC leaves your application vulnerable to unrepeatable reads as data shifts mid-flight, while SI famously opens the door to write skew, where two concurrent transactions update different halves of the same logical constraint.

Can we have our cake and eat it too? The paper introduces the Serial Safety Net (SSN), as a certifier that sits entirely on top of fast weak schemes like RC or SI, tracking the dependency graph and blessing a transaction only if it is serializable with respect to others.

SSN implementation

When a transaction T tries to commit, SSN calculates a low watermark $\pi(T)$ (the oldest transaction in the future that depends on T) and a high watermark $\eta(T)$ (the newest transaction in the past that T depends on). If $\pi(T) \le \eta(T)$, it means the past has collided with the future, and a dependency cycle has closed. SSN aborts the transaction.

Because SSN throws out any transaction that forms a cycle, the final committed history is mathematically guaranteed to be cycle-free, and hence Serializable (SER).

Subfigures (c) and (d) demonstrate SSN's safe conditions and its conservative trade-offs. In (c), the exclusion window is satisfied because the predecessor T3 committed before the low watermark $\pi(Tx)$, making it impossible for T3 to loop back as a successor. Subfigure (d), however, shows a false positive where transaction T3 is aborted because its exclusion window is violated, even though no actual cycle exists yet. This strictness is necessary, though: allowing T3 to commit would be dangerous, as a future transaction could silently close the cycle later without triggering any further warnings. Since SSN summarizes complex graphs into just two numbers ($\pi$ and $\eta$), it will sometimes abort a transaction simply because the exclusion window was violated, even if a true cycle hasn't formed yet.

SSN vs. Pure OCC

Now, you might be asking: Wait, this sounds a lot like Optimistic Concurrency Control (OCC), so why not just use standard OCC for Serializability?

Yes, SSN is a form of optimistic certification, but the mechanisms are different, and the evaluation section of the paper exposes exactly why SSN is a superior architecture for high-contention workloads.

Standard OCC does validation by checking exact read/write set intersections. If someone overwrote your data, you abort. The problem is the OCC Retry Bloodbath! When standard OCC aborts a transaction, retrying it often throws it right back into the exact same conflict because the overwriting transaction might still be active. In the paper's evaluation, when transaction retries were enabled, the standard OCC prototype collapsed badly, wasting over 60% of its CPU cycles just fighting over index insertions.

SSN, however, possesses the "Safe Retry" property. If SSN aborts your transaction T because a predecessor U violated the exclusion window, U must have already committed. When you immediately retry, the conflict is physically in the past; your new transaction simply reads $U$'s freshly committed data, bypassing the conflict entirely. SSN's throughput stays stable under pressure while OCC falls over.

Discussion

So what do we have here? SSN offers a nice way to get to SER, while keeping decent concurrency. It proves that with a little bit of clever timestamp math, you can turn a dirty high-speed concurrency scheme into a serializable one.

Of course, no system is perfect. If you are going to deploy SSN, you have to pay the piper. Here are some critical trade-offs.

To track these dependencies, SSN requires you to store extra timestamps on every single version of a tuple in your database. In a massive in-memory system, this metadata bloat is a significant cost compared to leaner OCC implementations.

SSN is also not a standalone silver bullet for full serializability. While it is great at tracking row-level dependencies on existing records, it does not natively track phantoms (range-query insertions). Because an acyclic dependency graph only guarantees serializability in the absence of phantoms , you cannot just drop SSN onto vanilla RC or SI; you must actively extend the underlying CC scheme with separate mechanisms like index versioning or key-range locking to prevent them.

To bring closure on the SSN approach, let's address one final architectural puzzle. If you've been following the logic so far, you might have noticed a glaring question. The paper demonstrates that layering SSN on top of Read Committed guarantees serializability (RC + SSN = SER). It also shows that doing the exact same thing with Snapshot Isolation gets you to the exact same destination (SI + SSN = SER). If both combinations mathematically yield a serializable database, why would we ever willingly pay the higher performance overhead of Snapshot Isolation? Why would we want SI+SSN when we have RC+SSN at home?

While layering SSN on top of Read Committed (RC) guarantees a serializable outcome, it exposes your application to in-flight problems. Under RC, reads simply return the newest committed version of a record and never block. This means the underlying data can change right under your application's feet while the transaction is running. Your code might read Account A, and milliseconds later read Account B after a concurrent transfer committed, seeing a logically impossible total, an inconsistent snapshot. Even though SSN will ultimately catch this dependency cycle and safely abort the transaction during the pre-commit phase, your application logic might crash before it ever reaches that protective exit door. Furthermore, even if your code survives the run, this late abort mechanism hides a big performance penalty: your system might burn a lot of CPU and memory executing a complex doomed transaction, only for SSN to throw all that wasted work at the final commit check.

This is why we gladly pay the extra concurrency control overhead for SI. Under SI, each transaction reads from a perfectly consistent snapshot of the database taken at its start time. From your application's perspective, time stops, completely shielding your code from ever seeing those transiently broken states mid-flight. However, as we mentioned in the beginning, SI still allows write skews, and pairing it with SSN covers for that to guarantee serializability. 

If you like to dive into this more, the authors later published a 20 page journal version here. I also found a recent follow up by Japanese researchers here.