a curated list of database news from authoritative sources

August 31, 2026

Murat Demirbas

The Safest Job from AI may be Writing

Today, tech folk are scrambling to change their workflows to meet newly inflated 5X productivity quotas, while getting pummeled under the cognitive debt of agent-generated code. With every new model release, the gap is widening and humans are becoming more of a bottleneck in the loop, approaching closer to obsolescence as "coders".

While the programmer's job description is getting completely refactored, writing remains surprisingly unaffected. LLMs have gotten very good at generating code, but I am appalled at the absolute shit they spew as prose. They always follow the same robotic cadence and cliches, and sprinkle the same tired vocabulary all around. They take my broken yet soulful writing and transform it into a plastic soulless word slop in the name of improving prose. Their writing communicates no actual understanding and insight. I think we are all developing a visceral ick reaction to AI writing. It is trapped in the uncanny valley, and it may be stuck there for a long time.

I am increasingly convinced LLMs will not threaten decent writers anytime soon. My prediction rests on the three observations below. Tell me where my logic breaks.


The plateau on prose

The stuck-in-slop state of LLM writing is not from lack of trying. AI labs already tried hard on improving prose and hit a wall. LLM giants would have loved to ship better writing capability to conquer marketing, copywriting, and publishing at zero marginal cost.

Look at image, voice, and heck video models. They got good quickly, because they can be scaled with more parameters and compute. Compared to their rapid progress, text models plateaued hard on expression, depth, and authenticity. I think it is wicked hard to bride the final 20% (also applies for image, voice, video models).


Writing is a wicked problem

In systems theory, a wicked problem is a problem that lacks a definitive formulation, a clear stopping rule, and an objectively correct solution. Writing is the ultimate wicked problem, because the context is constantly shifting, a piece is never truly finished editing, and the true metric for success is fundamentally subjective.

Mapping domains along this wickedness spectrum explains why AI dominates certain fields but produces utter slop in others:

  • Math sits on the left of the spectrum. Specifications are concise, and verification is binary and automated. Since the feedback loop is perfectly closed, AI models can rapidly solve math problems and prove results automatically.
  • Code relies on formal logic and test-driven feedback. An LLM can generate functional code because compilers, unit tests, and model checkers can instantly catch errors. Verification is largely mechanical.
  • Structured domains like law and finance also have some explicit boundaries as they are governed by regulatory frameworks and evaluated on empirical data.
  • Writing sits at the far extreme of the spectrum. There is no well defined specification to the task at hand, and there is no ground truth or objective verification of the output. The ultimate measure of success is resonance inside another human mind. This is why AI models fail to make progress on good writing.

  

Writing may be an AI-complete problem

Unlike coding, which is a single-mind interaction with a deterministic compiler, prose is a dual-mind problem governed by Theory of Mind. It requires the ability to continuously simulate a reader's internal mental state in real time. To write simply and persuasively, you must track what the reader already knows, manage their cognitive load sentence by sentence, and predict how an argument will land.

Since LLMs lack an active mental model of a specific human reader, they are just  optimizing for the statistical probability of the next word over a vast dataset. They cannot empathize with the human reader, as they don't have the human lived experience. And they have zero skin in the game.


Comparative advantage and costly signals 

To land this plane, let's pull in David Ricardo and classical economics. The law of comparative advantage states that even if one party can produce everything more efficiently than another, both still benefit from specializing where their relative opportunity cost is lowest. In other words, even if AI has an absolute advantage in typing speed and generating volume at zero marginal cost, our human labor is still governed by the opportunity cost of where our scarce resources would be least wasted.

The opportunity cost for a human burning their scarce cognitive capacity on generic and repetitive tasks is now infinitely high. Instead, human effort shines where AI fails, that is for navigating wicked-problems and pushing for creativity.

This is where economics meets evolutionary biology, as "human proof-of-work" becomes the ultimate costly signal. In nature, a costly signal (like a peacock’s tail or an elk's antlers) works because it is expensive to produce and impossible to fake. As AI slop saturates the web, with the same token (pardon my pun), the economic value shifts entirely to an authentic human voice.


Unlike tech folk, writers don't have to change a damn thing about how they work to optimize their comparative advantage and capture this costly signal. As AI is stripping away the accidental complexity of software to expose its inherent complexity, tech workers are struggling to adjust. But good writers have always been wrestling with the inherent complexity of communication at the wicked frontier, and they remain untouched. And maybe programming itself is becoming a form of writing: more opinionated, more architectural, and more about connecting with human intent.

by Murat (noreply@blogger.com)
Franck Pachot

PostgreSQL INCLUDE indexes: what problem are they trying to solve?

A common way to explain PostgreSQL's INCLUDE clause is that it helps with index-only scans. That's true, but it misses an important detail. Even before PostgreSQL 11, which introduced the INCLUDE clause, PostgreSQL was already capable of supporting covering indexes:

postgres=# create table demo ( id text primary key, value text)
;
CREATE TABLE

postgres=# insert into demo(id, value)
           select
             md5(g::text),       -- using text to see it with pageinspect
             md5((g%1000)::text) -- using text to see it with pageinspect
from generate_series(1,1000000) g
;
INSERT 0 1000000

postgres=# create index demo_idx1
           on demo(value, id)
;
CREATE INDEX

postgres=# vacuum analyze
;
VACUUM

postgres=# explain (verbose, analyze, buffers)
select id from demo
  where value <= '01'
;
                                                               QUERY PLAN
----------------------------------------------------------------------------------------------------------------------------------------
 Index Only Scan using demo_idx1 on public.demo  (cost=0.55..566.29 rows=8785 width=33) (actual time=0.008..0.551 rows=4000.00 loops=1)
   Output: id
   Index Cond: (demo.value <= '01'::text)
   Heap Fetches: 0
   Index Searches: 1
   Buffers: shared hit=50
 Query Identifier: -9119705436468283309
 Planning:
   Buffers: shared hit=5
 Planning Time: 0.118 ms
 Execution Time: 0.710 ms

The Index Only Scan covers all filtering (Index Cond: (demo.value <= '01'::text)) and projection (Output: id) without an INCLUDE clause.

Here is another example with output in PostgreSQL 8.4 and 9.3. Index-only scan for B-tree indexes was introduced in 9.2, and INCLUDE came later in 11.

This proves that you don't need an INCLUDE clause to create a covering index for a query. The same is true for other databases: Oracle users have built covering indexes that way for decades without an equivalent to the INCLUDE clause. Adding extra columns to the index can eliminate table access when the query needs those column values.

So why did PostgreSQL introduce a new syntax?

Let's create the covering index using an INCLUDE clause:

postgres=# create index demo_idx2
  on demo(value) include (id)
;
CREATE INDEX

The planner chooses it because the estimated cost is slightly lower:

postgres=# explain (verbose, analyze, buffers)
select id from demo
  where value <= '01'
;
                                                               QUERY PLAN
----------------------------------------------------------------------------------------------------------------------------------------
 Index Only Scan using demo_idx2 on public.demo  (cost=0.55..566.29 rows=8785 width=33) (actual time=0.015..1.011 rows=4000.00 loops=1)
   Output: id
   Index Cond: (demo.value <= '01'::text)
   Heap Fetches: 0
   Index Searches: 1
   Buffers: shared hit=50
 Query Identifier: -9119705436468283309
 Planning:
   Buffers: shared hit=5
 Planning Time: 0.132 ms
 Execution Time: 1.323 ms
(11 rows)

The two indexes have the same size in this example:

postgres=# select relname, pg_size_pretty(pg_relation_size(oid))
           from pg_class where relname in ('demo_idx1','demo_idx2')
;
  relname  | pg_size_pretty
-----------+----------------
 demo_idx2 | 91 MB
 demo_idx1 | 91 MB

Both indexes store value and id in their leaf tuples, so both can support index-only scans. The difference is in the B-tree key space. For demo_idx1, ordering is based on (value, id, TID), so both user columns participate in navigation. For demo_idx2, ordering is based on (value, TID), and id is stored as additional payload and is therefore absent from pivot tuples and other upper B-tree levels.

This is visible in the number of index key attributes:

postgres=# select indnatts, indnkeyatts from pg_index 
           where indexrelid='demo_idx1'::regclass
;
 indnatts | indnkeyatts
----------+-------------
        2 |           2


postgres=# select indnatts, indnkeyatts from pg_index 
           where indexrelid='demo_idx2'::regclass
;
 indnatts | indnkeyatts
----------+-------------
        2 |           1

Pageinspect can show more details

I check the index names and enable the extension:

postgres=# \d demo

              Table "public.demo"
 Column | Type | Collation | Nullable | Default
--------+------+-----------+----------+---------
 id     | text |           | not null |
 value  | text |           |          |
Indexes:
    "demo_pkey" PRIMARY KEY, btree (id)
    "demo_idx1" btree (value, id)
    "demo_idx2" btree (value) INCLUDE (id)

postgres=# create extension if not exists pageinspect
;
CREATE EXTENSION

Here are some entries from an internal page of the B-tree with all columns in the key:

postgres=# select * from bt_multi_page_stats('demo_idx1', 1, -1)     
           where type='i' order by blkno desc limit 1
\gset
postgres=# select itemoffset, ctid, itemlen, nulls, vars, dead, htid, encode(decode(replace(substr(data,4),' ',''), 'hex'),'escape'), data
           from bt_page_items('demo_idx1', :blkno) order by itemoffset limit 4
;

 itemoffset |   ctid    | itemlen | nulls | vars | dead | htid |                                          encode                                           |                                                                                                          data
------------+-----------+---------+-------+------+------+------+-------------------------------------------------------------------------------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
          1 | (11666,0) |       8 | f     | f    |      |      |                                                                                           |
          2 | (11667,2) |      80 | f     | t    |      |      | ffeabd223de0d4eacb9a3e6e53e5448dCe370679455dd6faf22304e9943c1f2fa\000\000\000\000\000\000 | 43 66 66 65 61 62 64 32 32 33 64 65 30 64 34 65 61 63 62 39 61 33 65 36 65 35 33 65 35 34 34 38 64 43 65 33 37 30 36 37 39 34 35 35 64 64 36 66 61 66 32 32 33 30 34 65 39 39 34 33 63 31 66 32 66 61 00 00 00 00 00 00
          3 | (11668,2) |      80 | f     | t    |      |      | ffeabd223de0d4eacb9a3e6e53e5448dCf9ae9b3ef06aa649c69149c580697d44\000\000\000\000\000\000 | 43 66 66 65 61 62 64 32 32 33 64 65 30 64 34 65 61 63 62 39 61 33 65 36 65 35 33 65 35 34 34 38 64 43 66 39 61 65 39 62 33 65 66 30 36 61 61 36 34 39 63 36 39 31 34 39 63 35 38 30 36 39 37 64 34 34 00 00 00 00 00 00
(3 rows)

You can recognize the same value (ffeabd223de0d4eacb9a3e6e53e5448d) for two id (e370679455dd6faf22304e9943c1f2fa and f9ae9b3ef06aa649c69149c580697d44)

Here are entries from a leaf page of this index:

postgres=# select * from bt_multi_page_stats('demo_idx1', 1, -1)     
           where type='l' order by blkno desc limit 1
\gset
postgres=# select itemoffset, ctid, itemlen, nulls, vars, dead, htid, encode(decode(replace(substr(data,4),' ',''), 'hex'),'escape'), data
           from bt_page_items('demo_idx1', :blkno) order by itemoffset limit 4
;
 itemoffset |   ctid    | itemlen | nulls | vars | dead |   htid    |                                          encode                                           |                                                                                                          data
------------+-----------+---------+-------+------+------+-----------+-------------------------------------------------------------------------------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
          1 | (2574,81) |      80 | f     | t    | f    | (2574,81) | ffeabd223de0d4eacb9a3e6e53e5448dCf9ae9b3ef06aa649c69149c580697d44\000\000\000\000\000\000 | 43 66 66 65 61 62 64 32 32 33 64 65 30 64 34 65 61 63 62 39 61 33 65 36 65 35 33 65 35 34 34 38 64 43 66 39 61 65 39 62 33 65 66 30 36 61 61 36 34 39 63 36 39 31 34 39 63 35 38 30 36 39 37 64 34 34 00 00 00 00 00 00
          2 | (10612,3) |      80 | f     | t    | f    | (10612,3) | ffeabd223de0d4eacb9a3e6e53e5448dCfa133607fa7a0fc0aa0c4eb5af973b0e\000\000\000\000\000\000 | 43 66 66 65 61 62 64 32 32 33 64 65 30 64 34 65 61 63 62 39 61 33 65 36 65 35 33 65 35 34 34 38 64 43 66 61 31 33 33 36 30 37 66 61 37 61 30 66 63 30 61 61 30 63 34 65 62 35 61 66 39 37 33 62 30 65 00 00 00 00 00 00
          3 | (1291,4)  |      80 | f     | t    | f    | (1291,4)  | ffeabd223de0d4eacb9a3e6e53e5448dCfa684bc1a44ca31270e620437a302582\000\000\000\000\000\000 | 43 66 66 65 61 62 64 32 32 33 64 65 30 64 34 65 61 63 62 39 61 33 65 36 65 35 33 65 35 34 34 38 64 43 66 61 36 38 34 62 63 31 61 34 34 63 61 33 31 32 37 30 65 36 32 30 34 33 37 61 33 30 32 35 38 32 00 00 00 00 00 00
          4 | (2994,61) |      80 | f     | t    | f    | (2994,61) | ffeabd223de0d4eacb9a3e6e53e5448dCfa81207e0ef8bf7c472f22d1093f9d8c\000\000\000\000\000\000 | 43 66 66 65 61 62 64 32 32 33 64 65 30 64 34 65 61 63 62 39 61 33 65 36 65 35 33 65 35 34 34 38 64 43 66 61 38 31 32 30 37 65 30 65 66 38 62 66 37 63 34 37 32 66 32 32 64 31 30 39 33 66 39 64 38 63 00 00 00 00 00 00
(4 rows)

You can recognize similar data. The leaves simply add the TID, which is exposed here as htid (heap tuple identifier). The entries are ordered by (value, id):

 fe9fc289c3ff0af142b6d3bead98a923 c8ea21e50b29b5e7081dd060e311fc7f (2574,81)
 fe9fc289c3ff0af142b6d3bead98a923 b22ba7ef4b85c722a92da83a480dd63f (10612,3)
 fe9fc289c3ff0af142b6d3bead98a923 b24f3bf60138d0b322d72be638626170 (1291,4)
 fe9fc289c3ff0af142b6d3bead98a923 b35b3291bb326500fbf6237f593f56ff (2994,61)

Let's look at the other index where id is in INCLUDE rather than the key. The leaves have similar length and format:

postgres=# select * from bt_multi_page_stats('demo_idx2', 1, -1)     
           where type='l' order by blkno desc limit 1
\gset
postgres=# select itemoffset, ctid, itemlen, nulls, vars, dead, htid, encode(decode(replace(substr(data,4),' ',''), 'hex'),'escape'), data
           from bt_page_items('demo_idx2', :blkno) order by itemoffset limit 4
;
 itemoffset |    ctid    | itemlen | nulls | vars | dead |    htid    |                                          encode                                           |                                                                                                          data
------------+------------+---------+-------+------+------+------------+-------------------------------------------------------------------------------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
          1 | (12081,14) |      80 | f     | t    | f    | (12081,14) | ffeabd223de0d4eacb9a3e6e53e5448dCe54b7a956b88f1a26234f9666332f40f\000\000\000\000\000\000 | 43 66 66 65 61 62 64 32 32 33 64 65 30 64 34 65 61 63 62 39 61 33 65 36 65 35 33 65 35 34 34 38 64 43 65 35 34 62 37 61 39 35 36 62 38 38 66 31 61 32 36 32 33 34 66 39 36 36 36 33 33 32 66 34 30 66 00 00 00 00 00 00
          2 | (12093,42) |      80 | f     | t    | f    | (12093,42) | ffeabd223de0d4eacb9a3e6e53e5448dC65e6c0b6c51f50809d390bd6af75262f\000\000\000\000\000\000 | 43 66 66 65 61 62 64 32 32 33 64 65 30 64 34 65 61 63 62 39 61 33 65 36 65 35 33 65 35 34 34 38 64 43 36 35 65 36 63 30 62 36 63 35 31 66 35 30 38 30 39 64 33 39 30 62 64 36 61 66 37 35 32 36 32 66 00 00 00 00 00 00
          3 | (12105,70) |      80 | f     | t    | f    | (12105,70) | ffeabd223de0d4eacb9a3e6e53e5448dC0053cd459922f1a843b5af3e5b384c61\000\000\000\000\000\000 | 43 66 66 65 61 62 64 32 32 33 64 65 30 64 34 65 61 63 62 39 61 33 65 36 65 35 33 65 35 34 34 38 64 43 30 30 35 33 63 64 34 35 39 39 32 32 66 31 61 38 34 33 62 35 61 66 33 65 35 62 33 38 34 63 36 31 00 00 00 00 00 00
          4 | (12118,17) |      80 | f     | t    | f    | (12118,17) | ffeabd223de0d4eacb9a3e6e53e5448dC37b9ccdafd5e83b27cf23bb1e0089e63\000\000\000\000\000\000 | 43 66 66 65 61 62 64 32 32 33 64 65 30 64 34 65 61 63 62 39 61 33 65 36 65 35 33 65 35 34 34 38 64 43 33 37 62 39 63 63 64 61 66 64 35 65 38 33 62 32 37 63 66 32 33 62 62 31 65 30 30 38 39 65 36 33 00 00 00 00 00 00
(4 rows)

However, can see that the entries are ordered by (value, TID) even if id values are present in the index entries:

 ffeabd223de0d4eacb9a3e6e53e5448d (12081,14) e54b7a956b88f1a26234f9666332f40f
 ffeabd223de0d4eacb9a3e6e53e5448d (12093,42) 65e6c0b6c51f50809d390bd6af75262f
 ffeabd223de0d4eacb9a3e6e53e5448d (12105,70) 0053cd459922f1a843b5af3e5b384c61
 ffeabd223de0d4eacb9a3e6e53e5448d (12118,17) 37b9ccdafd5e83b27cf23bb1e0089e63

That's one physical difference between the two indexes: the sort order. The columns in INCLUDE are not part of the key. They are just additional payload. This has some pros and cons that we will cover later.

There's another difference in the B-tree internal pages (root and branches) which store key ranges:

postgres=# select * from bt_multi_page_stats('demo_idx2', 1, -1)     
           where type='i' order by blkno desc limit 1
\
                                    
                                    
                                    

                                        by Franck Pachot
Percona Database Performance Blog

Rotating Expiring X.509 Certificates in Percona Server for MongoDB with Minimal Service Interruption

Expired TLS certificates can prevent new client connections and, when X.509 is used for Percona Server for MongoDB internal authentication, also prevent members of a replica set or sharded cluster from authenticating to one another. In this post we will discuss performing a same-CA renewal: replacement certificates for server, member, and client leaf are issued … Continued

The post Rotating Expiring X.509 Certificates in Percona Server for MongoDB with Minimal Service Interruption appeared first on Percona.

by Ivan Groenewold

August 27, 2026

Percona Database Performance Blog

Benchmarking vector indexes

Nearly every database has vector search now, and every one of them has a blog post with a big number in it. Almost none of those numbers can be checked, because the thing that makes them meaningful is usually missing. We built a vector-bench to stop guessing. You name the engines you want, build them … Continued

The post Benchmarking vector indexes appeared first on Percona.

by Evgeniy Patlan
Percona Database Performance Blog

Performance Progression of Percona Server for MySQL 8.4

1. Purpose and scope This performance investigation aims to look into the read/write performance of Percona Server for MySQL 8.4 and how it changed between versions released in 2026: 8.4.8-8 released on 12 March 2026 8.4.10-10 released on 30 June 2026 8.4.11-11 released on 20 August 2026 We want to see if there are improvements … Continued

The post Performance Progression of Percona Server for MySQL 8.4 appeared first on Percona.

by Bogdan Degtyariov
Murat Demirbas

Composition and Modular Verification of TLA+ specs

TLA+ is compositional in the abstract sense... In the astral plane, a program execution is an infinite sequence of states, each state giving a value to every variable in an imagined universal state space. A spec is a predicate (yes/no test) on executions, which denotes a set of allowed executions. In this setup, the steps that change variables in other specs look like stuttering to yours. And that enables us to denote composition as a beautiful purely logical conjunction, Spec1 /\ Spec2.

The problem is, this is too pure. When you try to model check a conjunction of two specs, your astral travel gets grounded. Since TLC only accepts specs in the normal form Init /\ [][Next]_vars, you need to manually expand the conjunction of two boxed formulas as: 
[][N1]_v1 /\ [][N2]_v2  =  []((N1 \/ UNCHANGED v1) /\ (N2 \/ UNCHANGED v2))

Expanding this gives us joint steps for N1/\N2, solo steps for each side, and both side stutter steps (which can be omitted vacuously). However, shared read/write variables between N1 and N2 cause problems (which we have ignored conveniently in the first paragraph, and now it is time to face them). Suppose a producer and a consumer share a channel. The naive producer spec Init /\ [][PNext]_<<chan, produced>> says: if chan changes, it was one of my actions. If you conjoin that with a consumer that also writes chan, you have specified a system where the consumer can never take a value. Conjunction of closed specs over shared state leads to over-constraining like that.


Open specs

The fix is to write each component as an "open" spec, a term I should define, since it has taken some damage lately. In an open spec, every step is either one of my actions or an environment change I have agreed to live with. E.g., in the producer component, EnvTake is the producer's "rely", i.e., the changes it tolerates from the rest of the universe. Yep, this is pretty much rely-guarantee reasoning: the Env action is the assumption/rely, and your actions plus your invariants are the guarantee.

Send    == chan = NoVal /\ chan' = produced /\ produced' = produced + 1

                        /\ UNCHANGED acked

EnvTake == chan # NoVal /\ chan' = NoVal /\ acked' = acked + 1

                        /\ UNCHANGED produced

Spec == Init /\ [][Send \/ EnvTake]_<<chan, acked, produced>>

PSync == /\ (chan = NoVal) => (produced = acked)

         /\ (chan # NoVal) => /\ produced = acked + 1

                              /\ chan = produced - 1


The consumer specification is symmetrical and straightforward.

Recv == /\ chan # NoVal /\ consumed' = Append(consumed, chan) 

        /\ acked' = acked + 1 /\ chan' = NoVal

EnvPut == /\ chan = NoVal /\ acked < MaxSend 

        /\ chan' = acked /\ UNCHANGED <<acked, consumed>>

Spec == Init /\ [][Recv \/ EnvPut]_<<chan, acked, consumed>>

CSync == acked = Len(consumed)


In the composition, you do the obvious thing. You drop each component's Env disjunct and replace it with the other component's concrete actions. The INSTANCE keyword allows us to refer to  Producer/Consumer formulas in the composed state space. The entire glue module is this:

P == INSTANCE Producer

C == INSTANCE Consumer

Init == P!Init /\ C!Init

Next == \/ (P!Send /\ UNCHANGED consumed)

        \/ (C!Recv /\ UNCHANGED produced)

PSpecOK == P!Spec

CSpecOK == C!Spec


Note that dropping the Envs and composing like this works only legitimate if each side's concrete actions are behaviors the other side's Env permitted. That's the obligation we state in the discharge module. The same two INSTANCE lines appear in the discharge module below to denote the obligations that each component's actions must imply the other's Env action. That is, the consumer's Recv must be a legal EnvTake from the producer's point of view, and vice versa.

vars == <<chan, acked, produced, consumed>>

DischargeTake == [][ (C!Recv /\ UNCHANGED produced) => P!EnvTake ]_vars

DischargePut  == [][ (P!PSync /\ P!Send /\ UNCHANGED consumed) => C!EnvPut ]_vars


Modular verification is doable

Modular verification is within reach of standard TLC, although it is rare to see it practiced due to feasibility reasons which I will revisit at the end.

First, notice where the discharge obligations get used. In the composition, Recv => EnvTake must hold at every step the composed system takes, i.e., at every reachable state of the composed system. But computing those reachable states means building the composed state space, which is exactly what modular verification refuses to do. How do we work around this?

Below is a rely-guarantee workflow that achieves this. Note that our cross-component discharge obligations are single-step implications. This is guaranteed for safety relies, because an Env action is a predicate on state pairs. A liveness rely like "the environment eventually takes the value" would not fit in an action, and is out of scope here. So, instead of calculating the reachable states, we can check the obligations over the crudest enumerable over-approximation, "all type-correct states", and strengthen the hypothesis only when a counterexample forces us to.

Step 1. Model check each component alone, closed by its own Env. This has very small state space, as the other component's private state never appears. This establishes local invariants (PSync for the producer). And if your rely is strong enough, this establishes even some global properties. E.g., my consumer proves in-order delivery against its EnvPut.   

Step 2. Check the rely discharges as action implications over a "chaos universe", a throwaway spec whose Init admits every type-correct state and whose Next admits every type-correct transition. Checking [][Recv => EnvTake]_vars against chaos verifies the implication over all state pairs, without computing reachability.

TypeUniverse == /\ chan \in Vals \cup {NoVal}     /\ acked \in 0..MaxSend

     /\ produced \in 0..MaxSend     /\ consumed \in SeqUniverse

Init == TypeUniverse

Next == /\ chan' \in Vals \cup {NoVal}    /\ acked' \in 0..MaxSend

     /\ produced' \in 0..MaxSend   /\ consumed' \in SeqUniverse

ChaosSpec == Init /\ [][Next]_vars

\* The two discharge obligations are checked as properties here  

DischargeTake == [][ (C!Recv /\ UNCHANGED produced) => P!EnvTake ]_vars

DischargePut  == [][ (P!PSync /\ P!Send /\ UNCHANGED consumed) => C!EnvPut ]_vars 

Step 3. Conclude verification by induction. This one is a theoretical step, as you do not run TLC here. The argument is this: every step of the composition is one side's action, and by (2) that step is also the other side's Env step. So each step extends both open specs at once, and by induction the composition refines both, and thus every property established in (1) transfers to the composition. This may seem a bit circular: the producer's guarantee licenses the consumer's assumption, which licenses the producer's guarantee. But, the induction breaks the circle: each side's guarantee holds one step longer than the assumption it feeds, which is precisely the semantics of Abadi-Lamport's -+> operator.

Now let me come clear about the kink here, and the explanation for PSync in DischargePut obligation. My consumer's rely, "the environment delivers exactly the next expected value",  was too strong. Discharging it against the producer's Send over the chaos universe failed with the TLC counterexample "produced = 5, acked = 0", which means the producer is about to send value 5 to a consumer expecting value 0.

Note that only the chaos universe contains this state. No real execution contains it, because every Send bumps produced, every take bumps acked, and a one-slot channel keeps two such counters in lockstep (equal when the slot is empty, one apart when full). And that is the embodiment of PSync property.

PSync == /\ (chan = NoVal) => (produced = acked)

                /\ (chan # NoVal) => /\ produced = acked + 1

                /\ chan = produced - 1

I didn't pull PSync out of a hat. It is the Producer invariant we checked locally in step 1 for the Producer open specification. Since PSync mentions only producer-visible variables, the producer-alone check from step (1) establishes it for free. The dischargeable obligation becomes PSync /\ Send => EnvPut, and TLC confirms this.


Is it worth it?

Earlier I said modular verification is rarely seen in practice, for feasibility reasons. In 1997, Lamport wrote a paper titled "Composition: A Way to Make Proofs Harder", and as always he is on the money. The mainstream TLA+ answer to decomposition follows his advice. Instead of decompositional verification, the practiced approach is to write one abstract specification of the whole system and verify that. The monolith needs no Env actions, it can cut across component layers wherever modeling is most convenient, and TLC handles the state space without problems since the specs are written at high (often too high) levels of abstraction. This is much simpler than specifying components and conjoining them, with all the bookkeeping for shared variables and joint steps we did in this post. Moreover, the costs of modular verification land on the human upfront: decomposition is hard, interface abstraction is hard, and both must be finished before you can check anything.

Despite all this, I am coming to believe we should perform compositional and modular verification anyway, because the monolith buys its simplicity by ignoring the system's actual structure, and we should not trade away good system design to appease the verifier. Interfaces, ownership boundaries, and independently evolving components are not verification inconveniences, they are the system design. A verification habit that only works on monoliths trains us to specify protocols with the system design erased. And ignoring good design causes all sort of problems for sustainability and reusability of verification.

Let me try to explain this better. In an earlier post, "The Two Abstractions of System Design: Hide or Reduce", I argued that we conflate two abstractions: modularity abstraction hides (interfaces, encapsulation, vertical boundaries), while modeling abstraction reduces (cut the system to the minimal behavioral skeleton relevant to a property).

The rely-guarantee reasoning we used in this post is where the two abstractions meet and become a joint constraint. The modularity abstraction is the boundary: we split the specs into private versus interface variables, hiding produced from the consumer and consumed from the producer. The modeling abstraction is the Env actions. E.g., EnvPut is not an API for the producer, it is a reduction of the producer: the minimal behavioral skeleton of the entire producer relevant to the consumer's property.

In that post I noted that a well-designed artifact can sometimes serve simultaneously as a spec to refine against and a skeleton to reason from. In rely-guarantee this is our exact mechanism. The same EnvPut is used twice: as a skeleton when the consumer verifies against it, and as a contract when the producer's actions must be shown to refine it. 

So good interface design finds the seam where a modularity cut and a modeling slice coincide. Interface design is hard because it is the one place the two abstractions must agree. Instead of complaining that abstractions leak, the Env action specifies the behavior about which interleavings cross the boundary, and proves guarantees on top of it. 

With the LLMs helping us in verification, this is becoming feasible. And with the LLMs generating the code, which needs reusable modular verification, this is becoming necessary.


One more thing... TLAPS changes the economics

Everything above was standard TLC, with the assumption that proofs are expensive and impractical. But they no longer are, again thanks to LLMs.

I tried TLAPS on these obligations, with Claude writing the proofs for the discharge obligations, and tlapm checking them. I re-check these from the VSCode command palette to prove step/module, and it was very satisfying to watch them all turn green.

The benefits of proofs scale well. Proof effort tracks the length of the spec, not the size of the state space. In our case, the chaos-universe caps go away: PSync /\ Send => EnvPut now holds for all counters, all values, and all instantiations. Modularity also works well for TLAPS. Modular decomposition produces many small local lemmas instead of one big invariant, and even the paper induction from step (3) can be mechanized to make the whole composition argument a checked artifact. Modular proofs also handle change well. When a component is modified, the broken obligations tell you exactly which contract clauses changed.


Hillel Wayne (hi Hillel!) wrote an accessible introduction to composing TLA+ specifications with state machines: https://www.hillelwayne.com/post/composing-tla/

Also here is an excellent talk from Ron Pressler on composition and conjunction of specs:
https://www.youtube.com/watch?v=TP3SY0EUV2A

Finally I enjoyed discussing with Markus Kuppe and Ugur Yavuz about TLAPS!
by Murat (noreply@blogger.com)

August 26, 2026

Percona Database Performance Blog

Migrating Postgres: Solving A Puzzle That Shouldn’t Be Hard

These days there’s been a lot of talk about Postgres having an impact on “everything”. Whether it’s replacing legacy systems, creating a new greenfield project or even implementing it as a back-end to an agentic AI, Postgres is today’s poster child for innovation. So performing something as dull and straightforward as a database migration should … Continued

The post Migrating Postgres: Solving A Puzzle That Shouldn’t Be Hard appeared first on Percona.

by Robert Bernier
VillageSQL Blog

Announcing VillageSQL Server 0.0.6

VillageSQL Server 0.0.6 is now available. This release advances the mainline to MySQL Server 8.4.11 and adds support for MySQL Server 9.7.2 and Percona Server 8.4.10.
by Adam Levin

August 25, 2026

Percona Database Performance Blog

Replication Lag on AWS FSx: The Hidden EC2 Single-Flow Bandwidth Limit

A recent case in our Percona Support team started with a familiar complaint. A PostgreSQL standby lagging behind its primary. Although the problem was simple, it brought a specific flavor that’s worth sharing. The customer had already reached out to AWS Support about the storage layer behind the database, an Amazon FSx filesystem mounted over … Continued

The post Replication Lag on AWS FSx: The Hidden EC2 Single-Flow Bandwidth Limit appeared first on Percona.

by Pablo Svampa
Percona Database Performance Blog

Software Bill of Materials in Percona Server for MongoDB

Introduction A software bill of materials (SBOM) offers end users enhanced supply chain visibility, thereby facilitating license compliance and timely vulnerability detection. An SBOM of an application, library, or framework (collectively referred to as a “component”) is a machine-readable document that enumerates all other components it incorporates, including transitive ones. In this way, an SBOM … Continued

The post Software Bill of Materials in Percona Server for MongoDB appeared first on Percona.

by Konstantin Trushin

August 24, 2026

August 23, 2026

Murat Demirbas

Thoughts on LLMs

I am a distributed systems researcher. I mostly read and write about distributed systems and lightweight formal methods. But as my blog definition says, the blog is about "distributed systems broadly defined and other curiosities". 

The last two years, LLMs were unavoidably the biggest part of those curiosities. However, I was still surprised how much I had written about them, when I went looking for a line I remembered coining. Something like, "LLMs are good at mediocrity, but really fast".

I couldn't find the line, but instead I found a pile of my takes on LLMs scattered across the blog, and I figured it was worth collecting them into an index. So here it is, enjoy! I also threw in my overall take on LLMs that has stayed constant through their four years of reign so far.

 

Hot takes on LLMs

Our Collective Bike Shed Moment (June 26)

Are We Becoming Architects or Butlers to LLMs? (Feb 26)

How LLMs may affect academic writing (Feb 26) 

Agentic AI and The Mythical Agent-Month (Jan 26)

The Agentic Self: Parallels Between AI and Self-Improvement (Jan 26) 

Too Close to Our Own Image? (Jan 26)

Rethinking the University in the Age of AI (Jan 26)

Welcome to Town Al-Gasr (Jan 26)

The Invisible Curriculum of Research (Oct 25) — mostly about AI, trust me

Academic chat: On PhD (Oct 25) — follow-up to the above

What I'd do as a College Freshman in 2025 (Apr 25)


Hot damn, 11 posts deep... Apparently I am an AI thought leader now by accident.

Looking at the dates, I was clearly most obsessed with LLMs in January 2026. There is no surprise there, since agentic tools and models turned a real corner that Thanksgiving of 2025. 

What has stayed constant over the years, however, even as the models themselves got much better, is my verdict on them. The phrase I had been hunting for turned out to be: "LLMs excel at high-throughput mediocrity". 

LLM output looks excellent when you are not the expert in the room. But on a topic you actually know, you would evaluate the output only as a notch above mediocre. This is the Gell-Mann amnesia effect in action. However, the difference is that LLMs can produce this output fast, and they never get tired.  

That is actually very handy when you don't want to work on a part of a project that requires mediocre effort. And the best thing is, you don't have to get bogged down doing it, and keep your momentum going as the LLMs handle those parts. They are a gift from the Gods if you have ADHD. The mundane half of a project that used to stall me out completely is no longer an obstacle.

Which is all to say,  LLMs are a tool. Use the right tool for the right job and you'll love it. Master your tools, and don't focus on their shortcomings for everything and all things.

Even with all these tools running, my highest-ROI tool is still just Emacs (going strong against LLMs at 50 years old, like me), where the actual thinking, writing, and planning happens. Use LLMs for the uninteresting stuff, where mediocrity is sufficient, so you have your time and energy for the work that actually matters.


AI x Systems Research

Well, LLMs didn't just show up as a curiosity in my work, they also collided more directly with my research. Here as they show up in my paper reviews, workshop write-ups, and conference notes, where formal methods and AI actually crossed paths.


Specula: Scaling formal specifications for autonomous model checking of system code (August 26)

Our MongoDB TLA+ Workshop (June 26)

Writing Code vs. Shipping Code: Productivity Effects Across Generations of AI Coding Tools (June 26)

ACM CAIS: Conference on AI and Agentic Systems (June 26)

BugBash'26 Keynote: We won, what now? (April 26) 

Measuring Agents in Production (March 26)

Measuring AI Ability to Complete Long Software Tasks (March 26) 

SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems (March 26) 

Beat Paxos (March 26)

Barbarians at the Gate: How AI is Upending Systems Research (Oct 25)

Supporting our AI overlords: Redesigning data systems to be Agent-first (Sep 25)

Neurosymbolic AI: Why, What, and How (Aug 25)

by Murat (noreply@blogger.com)

August 20, 2026

AWS Database Blog - Amazon Aurora

Migrate multilingual full-text search from SQL Server to PostgreSQL

Migrating full-text search from SQL Server to PostgreSQL can silently change results because the engines handle text, linguistics, and accents differently. This post shows how to reproduce SQL Server full-text search on Amazon Aurora PostgreSQL and Amazon RDS for PostgreSQL, covering collation, tokenization, accent-insensitive search, and synonyms.
by Ken Zhang