a curated list of database news from authoritative sources

November 03, 2026

November 02, 2026

Franck Pachot

PostgreSQL document compression: TOAST thresholds, storage policies, and page size

A common way to store documents in PostgreSQL is a table with an ID and a JSONB column. The open-source DocumentDB extension instead stores BSON, the binary document format used by MongoDB, to provide more data types and MongoDB compatibility.

Both approaches commonly combine two patterns that do not perfectly fit what SQL databases were designed for:

  • Rows with a single variable-length column, whose values can range from a few dozen bytes to many megabytes.
  • Repeated data or metadata, such as similar field names and arrays of objects with the same schema, like time-series buckets.

MongoDB's storage engine, WiredTiger, packs many documents into B-tree leaf pages. The default maximum page sizes — 32 KB for leaf pages and 4 KB for internal pages — are limits on the uncompressed page image fed to the block compressor, not on individual documents: MongoDB configures leaf_value_max=64MB, so a document larger than 32 KB simply produces a larger leaf page rather than overflow storage. Snappy compresses each page image for ordinary collections (time-series collections use Zstd, which ignores the global compressor setting), and the compressed result is written in multiples of the 4 KB allocation_size. Because compression runs over the whole page image, several small documents — including their repeated field names — contribute redundant byte sequences to the same compression input.

A JSON or BSON document can contain substantial byte-sequence redundancy: repeated field names, common name prefixes, and repeated values or structures. LZ77-family compressors such as Snappy and LZ4 can replace matching sequences with backreferences to earlier bytes. They don't need to understand JSON, and matches aren't restricted to the beginning of a document.

Binary does not mean compressed: BSON includes field names, and repeated embedded objects repeat those names. JSONB can contain similar redundancy. PostgreSQL can compress those sequences in JSON, JSONB, or a BSON extension type. However, the decision to attempt compression is not driven by document redundancy. It belongs to TOAST's generic heap-row storage policy: reduce a wide row, trying column compression before storing permitted attributes externally in chunks.

This distinction matters for small documents. It also makes increasing the page size potentially counterproductive: the same document can stop being compressed on a larger-page build.

I will reproduce both effects, then compare the SQL controls with the hardcoded values. The examples use PostgreSQL 19 and core JSONB, so they can run without an extension or a custom patch. The distinction between whole-row activation and individual-column compression also applies to the TOAST-backed BSON values stored by DocumentDB.

What is compressed, and what is measured?

TOAST measures the whole tuple (row) to decide whether to start. However, compression acts on individual eligible column values, not on the entire row or all the documents in a page.

PostgreSQL's ordinary table storage uses fixed-size pages, 8 KB by default. A row cannot span those pages. Large column values can instead be moved to an associated TOAST table, and the main row then contains a pointer to access the chunks in the TOAST table by index scan.

JSONB still contains compressible byte sequences. It is a binary representation, not an already-compressed JSON string. Within one object, it normalizes key order and duplicate keys, but an array of similarly structured objects can repeat the same field names. No shared key dictionary exists across those objects or across independently stored JSONB rows.

The distinction between repeated names within a document and repeated names across documents is important. PostgreSQL compresses one column value at a time. PostgreSQL calls each value a datum in its source code. That per-datum compression can use the former repetition, not the latter.

MongoDB's WiredTiger storage engine uses Snappy block compression on disk by default for ordinary collections. Small documents can share a page, so one block-compression input can include repeated names and structures from several documents. This is not a separate compression call per small document. Other codecs can be configured, and time-series collections have different defaults. This is a difference in compression scope, not a capability reserved to Snappy.

This post measures stored datum representations, not table allocation or query performance. I use:

  • pg_column_size(doc::text::jsonb) to reconstruct an uncompressed logical JSONB datum for these ordinary JSON inputs
  • pg_column_compression(doc) to report the actual accepted method
  • pg_column_size(doc) for its stored representation
  • pg_column_toast_chunk_id(doc) IS NOT NULL to identify external values

The last function is available in PostgreSQL 19. For an external value, pg_column_size is not the inline pointer size. The on-disk pointer in the main row occupies 18 bytes. The external size excludes the outer four-byte varlena length word, which explains some four-byte differences below without attributing them to the codec.

Reproduce the environment and output

All SQL needed for the experiments is included below. Run the statements in order in a fresh test database. For each page-size comparison, start a separate PostgreSQL instance.

I use aligned ASCII output, with NULL displayed as (null). To reproduce that format, start an existing server's session with these options:

psql -X -P pager=off -P 'null=(null)' -P format=aligned \
  -P linestyle=ascii -P border=1 -U postgres -d postgres

These are the initial settings on the source-built 8 KB server:

postgres=# SHOW server_version;

 server_version 
----------------
 19rc1
(1 row)

postgres=# SHOW block_size;

 block_size 
------------
 8192
(1 row)

postgres=# SHOW default_toast_compression;

 default_toast_compression 
---------------------------
 lz4
(1 row)

The selected codec is explicit in every test. PostgreSQL 14-18's upstream default is pglz, but an LZ4-enabled PostgreSQL 19 RC1 build defaults to LZ4. SET COMPRESSION has been available since PostgreSQL 14.

LZ4 is a sensible starting choice when compression/decompression CPU matters, but the workload still determines the trade-off. It does not always produce the smallest result. DocumentDB's current setup/tuning configuration selects default_toast_compression = 'lz4' when supported. This is a launcher-chosen PostgreSQL setting, not a property of BSON, nor a guarantee that every installation is configured that way. Check the live server and column settings rather than assuming them from a product name.

A compressible document below the activation threshold

I construct a JSONB array containing eight objects with repeated temperature and humidity names. Both rows receive the same document. The only difference is an unrelated column stored PLAIN, so it cannot be compressed or moved externally.

postgres=# CREATE TABLE small_documents(
    id integer, doc jsonb, other text
);

CREATE TABLE

postgres=# ALTER TABLE small_documents
            ALTER COLUMN doc SET COMPRESSION lz4
;

ALTER TABLE

postgres=# ALTER TABLE small_documents
            ALTER COLUMN other SET STORAGE PLAIN
;

ALTER TABLE

postgres=# INSERT INTO small_documents
    SELECT id,
           jsonb_build_object('samples', (
             SELECT jsonb_agg(jsonb_build_object('temperature',20,'humidity',60))
             FROM generate_series(1,8)
           )),
           repeat('q', CASE id WHEN 1 THEN 0 ELSE 1600 END)
    FROM generate_series(1,2) AS g(id)
;

INSERT 0 2

postgres=# SELECT id,
           pg_column_size(doc::text::jsonb) AS logical_bytes,
           octet_length(other) AS other_bytes,
           pg_column_compression(doc) AS compression,
           pg_column_size(doc) AS stored_bytes,
           pg_column_toast_chunk_id(doc) IS NOT NULL AS external
    FROM small_documents ORDER BY id
;

 id | logical_bytes | other_bytes | compression | stored_bytes | external 
----+---------------+-------------+-------------+--------------+----------
  1 |           508 |           0 | (null)      |          508 | f
  2 |           508 |        1600 | lz4         |          109 | f
(2 rows)

The first 508-byte JSONB datum remains uncompressed. The second compresses to 109 bytes, even though its uncompressed document bytes are identical. The additional 1,600-byte column made the tuple large enough to enter TOAST processing.

This proves both points:

  1. Repeated field names and values in JSONB are compressible.
  2. PostgreSQL does not independently ask whether that small JSONB datum would benefit from compression. The enclosing tuple controls activation.

I used an unrelated column for academic purposes. Of course, I'm not suggesting that adding more data to trigger compression is a good idea.

The hardcoded gate is not the per-table target

In the PostgreSQL source, the ordinary values are derived as follows:

#define TOAST_TUPLES_PER_PAGE 4
#define TOAST_TUPLE_THRESHOLD MaximumBytesPerTuple(TOAST_TUPLES_PER_PAGE)
#define TOAST_TUPLE_TARGET TOAST_TUPLE_THRESHOLD

MaximumBytesPerTuple(4) accounts for page headers, line pointers, and alignment. It is not exactly block_size / 4. Here are the values for the default 8 KB page size and for PostgreSQL builds with 16 KB or 32 KB pages:

PostgreSQL page size Fixed tuple activation threshold Default tuple target Maximum native TOAST chunk payload
8,192 bytes 2,032 bytes 2,032 bytes 1,996 bytes
16,384 bytes 4,080 bytes 4,080 bytes 4,044 bytes
32,768 bytes 8,176 bytes 8,176 bytes 8,140 bytes

These are the values for the tested eight-byte-aligned builds. The chunk capacities were also observed from actual external data, not inferred from page size alone.

Both heap_prepare_insert and heap_update check the fixed threshold before invoking the toaster for fresh inline tuples. Inside the toaster, toast_tuple_target provides the reduction target, after subtracting tuple header overhead.

It’s not simply "compress when the row cannot fit on a page.” A tuple just over 2 KB can still fit on an 8 KB page. By default, wide rows are reduced earlier, with the goal of keeping their size consistent with roughly four tuples per page. This is a row-density and oversized-attribute policy, rather than a separately tunable document-compression policy.

These are fresh values with one eligible document column. If a row has several eligible columns, the toaster works in phases rather than compressing the entire row as one object.

Change the target without changing activation

The following input view constructs fresh JSONB values from repetitive text. It deliberately samples several payload sizes. It is not intended to represent a natural document distribution.

A view is used rather than copying stored compressed values from another table. Reusing an existing compressed datum would confound a test of whether the destination attempts compression.

postgres=# CREATE TEMP VIEW input_documents AS
    SELECT n, jsonb_build_object('v', repeat('x', 1024 * (1 << n))) AS doc
    FROM (VALUES (0),(1),(2),(6),(9),(10),(11)) AS sizes(n)
;

CREATE VIEW

postgres=# CREATE TABLE extended_default(
    n integer PRIMARY KEY, doc jsonb
);

CREATE TABLE

postgres=# CREATE TABLE extended_200(
    n integer PRIMARY KEY, doc jsonb
)
    WITH (toast_tuple_target=200)
;

CREATE TABLE

postgres=# CREATE TABLE extended_4k(
    n integer PRIMARY KEY, doc jsonb
)
    WITH (toast_tuple_target=4096)
;

CREATE TABLE

postgres=# ALTER TABLE extended_default
            ALTER COLUMN doc SET COMPRESSION lz4
;

ALTER TABLE

postgres=# ALTER TABLE extended_200
            ALTER COLUMN doc SET COMPRESSION lz4
;

ALTER TABLE

postgres=# ALTER TABLE extended_4k
            ALTER COLUMN doc SET COMPRESSION lz4
;

ALTER TABLE

postgres=# INSERT INTO extended_default
    SELECT * FROM input_documents ORDER BY n
;

INSERT 0 7

postgres=# INSERT INTO extended_200
    SELECT * FROM input_documents ORDER BY n
;

INSERT 0 7

postgres=# INSERT INTO extended_4k
    SELECT * FROM input_documents ORDER BY n
;

INSERT 0 7

postgres=# SELECT policy, 1 << n AS payload_kib,
           pg_column_compression(doc) AS compression,
           pg_column_size(doc) AS stored_bytes,
           pg_column_toast_chunk_id(doc) IS NOT NULL AS external
    FROM (
      SELECT 1 AS position, 'default' AS policy, * FROM extended_default
      UNION ALL SELECT 2,'target_200',* FROM extended_200
      UNION ALL SELECT 3,'target_4096',* FROM extended_4k
    ) AS cases
    ORDER BY position,n
;

   policy    | payload_kib | compression | stored_bytes | external 
-------------+-------------+-------------+--------------+----------
 default     |           1 | (null)      |         1041 | f
 default     |           2 | lz4         |           39 | f
 default     |           4 | lz4         |           47 | f
 default     |          64 | lz4         |          288 | f
 default     |         512 | lz4         |         2083 | t
 default     |        1024 | lz4         |         4139 | t
 default     |        2048 | lz4         |         8252 | t
 target_200  |           1 | (null)      |         1041 | f
 target_200  |           2 | lz4         |           39 | f
 target_200  |           4 | lz4         |           47 | f
 target_200  |          64 | lz4         |          284 | t
 target_200  |         512 | lz4         |         2083 | t
 target_200  |        1024 | lz4         |         4139 | t
 target_200  |        2048 | lz4         |         8252 | t
 target_4096 |           1 | (null)      |         1041 | f
 target_4096 |           2 | (null)      |         2065 | f
 target_4096 |           4 | lz4         |           47 | f
 target_4096 |          64 | lz4         |          288 | f
 target_4096 |         512 | lz4         |         2087 | f
 target_4096 |        1024 | lz4         |         4139 | t
 target_4096 |        2048 | lz4         |         8252 | t
(21 rows)

The default JSONB storage strategy is EXTENDED, which permits both compression and external storage.

Three observations distinguish the decisions:

  • Even with a 200-byte target, the 1 KB-payload document still remains uncompressed and inline at 1,041 bytes. Its tuple did not enter TOAST because it is smaller than the hardcoded MaximumBytesPerTuple(4).
  • Once TOAST is active, lowering the target externalizes values sooner: the 64 KB payload is inline with the default target but external with the 200-byte target.
  • With a 4 KB target, the 2 KB-payload document remains uncompressed at 2,065 bytes. Its tuple enters TOAST, but already meets the larger target. The same document compressed to 39 bytes in the other two tables.

Raising the target is therefore not an independent "retain more compressed documents inline" control. It can also prevent a compression attempt.

The default and 200-byte cases report 288 and 284 bytes respectively for the same compressed 64 KB-payload document. This is the inline/external varlena accounting difference, not a better compression result.

Storage strategies: what SQL can control

There are four column storage strategies:

Strategy Compression External storage
EXTENDED Permitted, attempted in the first phase when reduction is needed Permitted
EXTERNAL Not permitted Permitted
MAIN Permitted, attempted in a later phase when needed Last resort
PLAIN Not permitted Not permitted

MAIN does not guarantee inline storage. MAIN attributes are also skipped during the first compression pass: they get their own compression round only after EXTENDED/EXTERNAL attributes have been compressed and externalized. They are likewise skipped by the out-of-line loops until the last-resort pass, which uses TOAST_TUPLE_TARGET_MAIN (MaximumBytesPerTuple(1) ≈ 8,160 bytes on an 8 KB build). EXTERNAL does not mean "externalize every document,” and an explicit LZ4 method cannot override its prohibition on compression.

Here EXTERNAL and MAIN use the same 4 KB target, making the comparison independent of an accidental target difference:

postgres=# CREATE TABLE external_4k(
    n integer PRIMARY KEY, doc jsonb
)
    WITH (toast_tuple_target=4096)
;

CREATE TABLE

postgres=# CREATE TABLE main_4k(
    n integer PRIMARY KEY, doc jsonb
)
    WITH (toast_tuple_target=4096)
;

CREATE TABLE

postgres=# CREATE TABLE plain_case(
    n integer PRIMARY KEY, doc jsonb
);

CREATE TABLE

postgres=# ALTER TABLE external_4k
            ALTER COLUMN doc SET COMPRESSION lz4
;

ALTER TABLE

postgres=# ALTER TABLE main_4k
            ALTER COLUMN doc SET COMPRESSION lz4
;

ALTER TABLE

postgres=# ALTER TABLE plain_case
            ALTER COLUMN doc SET COMPRESSION lz4
;

ALTER TABLE

postgres=# ALTER TABLE external_4k
            ALTER COLUMN doc SET STORAGE EXTERNAL
;

ALTER TABLE

postgres=# ALTER TABLE main_4k
            ALTER COLUMN doc SET STORAGE MAIN
;

ALTER TABLE

postgres=# ALTER TABLE plain_case
            ALTER COLUMN doc SET STORAGE PLAIN
;

ALTER TABLE

postgres=# INSERT INTO external_4k
    SELECT * FROM input_documents ORDER BY n
;

INSERT 0 7

postgres=# INSERT INTO main_4k
    SELECT * FROM input_documents ORDER BY n
;

INSERT 0 7

postgres=# INSERT INTO plain_case
    SELECT * FROM input_documents WHERE n<=2 ORDER BY n
;

INSERT 0 3

postgres=# SELECT policy, 1 << n AS payload_kib,
           pg_column_compression(doc) AS compression,
           pg_column_size(doc) AS stored_bytes,
           pg_column_toast_chunk_id(doc) IS NOT NULL AS external
    FROM (
      SELECT 1 AS position,'EXTERNAL' AS policy,* FROM external_4k
      UNION ALL SELECT 2,'MAIN',* FROM main_4k
      UNION ALL SELECT 3,'PLAIN',* FROM plain_case
    ) AS cases
    ORDER BY position,n
;

  policy  | payload_kib | compression | stored_bytes | external 
----------+-------------+-------------+--------------+----------
 EXTERNAL |           1 | (null)      |         1041 | f
 EXTERNAL |           2 | (null)      |         2065 | f
 EXTERNAL |           4 | (null)      |         4109 | t
 EXTERNAL |          64 | (null)      |        65549 | t
 EXTERNAL |         512 | (null)      |       524301 | t
 EXTERNAL |        1024 | (null)      |      1048589 | t
 EXTERNAL |        2048 | (null)      |      2097165 | t
 MAIN     |           1 | (null)      |         1041 | f
 MAIN     |           2 | (null)      |         2065 | f
 MAIN     |           4 | lz4         |           47 | f
 MAIN     |          64 | lz4         |          288 | f
 MAIN     |         512 | lz4         |         2087 | f
 MAIN     |        1024 | lz4         |         4143 | f
 MAIN     |        2048 | lz4         |         8252 | t
 PLAIN    |           1 | (null)      |         1041 | f
 PLAIN    |           2 | (null)      |         2065 | f
 PLAIN    |           4 | (null)      |         4113 | f
(17 rows)

For EXTERNAL, the 2 KB payload is still inline, but the 4 KB payload is external without compression.

For MAIN, the 1 MB payload compresses to 4,143 inline bytes. It can stay inline because MAIN postpones externalization to its last-resort target: the maximum tuple size that fits on one page. The larger 2 MB-payload document still becomes external after compression.

For PLAIN, no value compresses or becomes external. A row that cannot fit on the heap page fails. Run this separate statement expecting an error:

postgres=# INSERT INTO plain_case
    VALUES (3,jsonb_build_object('v',repeat('x',8192)))
;

ERROR:  54000: row is too big: size 8240, maximum size 8160
LOCATION:  RelationGetBufferForTuple, hio.c:531

The 8,160-byte maximum in this error is the heap-page tuple limit, not the 2,032-byte TOAST activation threshold. They answer different questions.

This is the complete SQL control surface relevant to these cases:

Control Scope Changes the fixed activation threshold?
ALTER COLUMN ... SET STORAGE ... Column's permitted/preferred representation No
ALTER COLUMN ... SET COMPRESSION pglz/lz4 Codec when compression is attempted No
default_toast_compression Default codec when the column has no override No
ALTER TABLE ... SET (toast_tuple_target=...) Whole-tuple reduction target after entry No
TOAST_TUPLE_THRESHOLD, TOAST_TUPLES_PER_PAGE Compiled activation policy Source change
TOAST_MAX_CHUNK_SIZE, EXTERN_TUPLES_PER_PAGE Compiled external chunk capacity Separate from activation
BLCKSZ Compiled page size Changes several defaults together

Changing page and chunk sizes requires a freshly initialized cluster. They are not runtime GUCs. Changing only a main-tuple threshold is not inherently an on-disk page-format change, but a correct implementation still has to consider all heap entry paths and TOAST-table creation.

The compression algorithm still matters after activation

Compression is an attempt, not a storage guarantee. Pglz's default strategy has a 32-byte minimum input, a 25% minimum reduction policy, and a 1,024-byte encoded-output first-success limit: it aborts if it has emitted that much without finding a match.

Those are pglz strategy rules, not user-configurable document thresholds. LZ4 does not impose pglz's first-success or minimum-rate rules. Both must still pass TOAST's header/alignment savings check.

Changing the column codec does not rewrite existing values:

postgres=# CREATE TABLE codec_example(
    id integer PRIMARY KEY, doc jsonb
);

CREATE TABLE

postgres=# ALTER TABLE codec_example
            ALTER COLUMN doc SET COMPRESSION pglz
;

ALTER TABLE

postgres=# INSERT INTO codec_example
    VALUES
      (1,jsonb_build_object('v',repeat('x',4096)))
;

INSERT 0 1

postgres=# ALTER TABLE codec_example
            ALTER COLUMN doc SET COMPRESSION lz4
;

ALTER TABLE

postgres=# INSERT INTO codec_example
    VALUES
      (2,jsonb_build_object('v',repeat('x',4096)))
;

INSERT 0 1

postgres=# SELECT id, pg_column_compression(doc) AS compression,
           pg_column_size(doc) AS stored_bytes
    FROM codec_example ORDER BY id
;

 id | compression | stored_bytes 
----+-------------+--------------
  1 | pglz        |           71
  2 | lz4         |           47
(2 rows)

The old value remains pglz. The freshly constructed new value uses LZ4. An update that leaves the document unchanged, or a copy of an already compressed datum, need not recompress it. Therefore, changing the setting is not proof that existing data now uses the new codec.

Larger pages: fewer documents become compression candidates

Larger pages can reduce the number of external chunks. That does not mean they preserve compression behavior.

I rebuilt PostgreSQL 19 RC1 with --with-blocksize=8, 16, and 32, keeping the other configure options the same, then initialized fresh clusters.

Do not reuse a data directory across page sizes. A different page size also requires rebuilding linked extensions against that PostgreSQL installation. This comparison deliberately uses core JSONB rather than mixing extension versions or a stock image with a different source-built baseline.

8 KB: all but the smallest repeated-field document compress

The samples array now contains 8, 64, 128, or 256 similarly structured objects. All tests explicitly select LZ4. One table retains the build's default target. The other sets it to 2040.

postgres=# CREATE TEMP VIEW page_inputs AS
    SELECT n, jsonb_build_object
                                    
                                    
                                    

                                        by Franck Pachot
Percona Database Performance Blog

An alternative to sharding a MongoDB replica set that outgrew its memory: a proof of concept

An alternative to sharding a MongoDB replica set that outgrew its memory: a proof of concept A replica set that no longer fits in memory Most MongoDB replica sets start small. The working set fits in the WiredTiger cache, reads come from memory, and nobody thinks about disks. Then the data keeps growing. Orders, events … Continued

The post An alternative to sharding a MongoDB replica set that outgrew its memory: a proof of concept appeared first on Percona.

by Zelmar Michelini
AWS Database Blog - Amazon Aurora

AWS contributes a large-transaction binary log optimization to MySQL

When MySQL commits a large transaction, writing it to the binary log can freeze every other commit on the server for minutes. This post introduces Binary Log Optimization for Large Transactions (BOLT), an AWS contribution to community MySQL that makes commit latency independent of transaction size, speeds crash recovery, and improves throughput.
by Xueting Wu
VillageSQL Blog

How VillageSQL does open source

VillageSQL plans and builds VillageSQL Server, the open source MySQL fork that adds an extension framework, in public, and every contributor follows the same written rules.
by Adam Levin

November 01, 2026

Percona Database Performance Blog

Multi-Node Unused Index Verification

Every MySQL schema that’s been around for a few years collects indexes nobody remembers adding. Some were for a report that was retired. Some came from an ORM migration. A few were added “just in case” and never used. They all cost something: extra writes on every INSERT and UPDATE, increased buffer pool pressure, larger … Continued

The post Multi-Node Unused Index Verification appeared first on Percona.

by Arunjith Aravindan

October 30, 2026

Percona Database Performance Blog

What’s New in PSMDB Sandbox: Six Months of Updates

Earlier this year, we introduced PSMDB Sandbox, a lightweight web UI that sits on top of our Terraform and Ansible automation for MongoDB. Since then, the project has changed a lot. It has a new name and repository, and it supports many more Percona products, MongoDB features and platforms. In this post, I will go … Continued

The post What’s New in PSMDB Sandbox: Six Months of Updates appeared first on Percona.

by Ivan Groenewold

October 29, 2026

VillageSQL Blog

Village News: MySQL News + Events (29 October 2026)

Welcome back to Village News, our curated roundup of MySQL and database news. This week, plans for FOSDEM 2027 took shape, with a new M-Ecosystem devroom and MySQL Belgian Days opening their calls for papers.

If you want to get these updates, just subscribe to the blog.

Enjoy!

MySQL

by Dominic Preuss
Percona Database Performance Blog

Benchmarking Vector search in six database engines

We loaded 990,000 OpenAI embeddings of 1,536 dimensions into six databases that index vectors themselves, built an HNSW index in each, and measured five things: time to a queryable index, storage and memory, recall against throughput, throughput under concurrent clients, and what happens when 10% of the corpus is rewritten. Same host, same container shape, … Continued

The post Benchmarking Vector search in six database engines appeared first on Percona.

by Evgeniy Patlan
Stack - Convex Blog

Turns out database backups are NOT trivial

I thought backing up a database was simple, you just loop over the tables and copy the rows out. Nipunn sat me down at a whiteboard and showed me why that can give you a backup of data that never existed, and how Convex gets around it.
by Stack
Percona Database Performance Blog

PLGM Has Grown Up: A New UI and Many More Features

Back in December I introduced Percona Load Generator for MongoDB Clusters (PLGM), a benchmark tool built around one idea: test your database with your own schema and your own queries, not some random data. At the time, PLGM was a command-line tool. You edited a YAML file, ran the binary, and read the numbers in … Continued

The post PLGM Has Grown Up: A New UI and Many More Features appeared first on Percona.

by Daniel Almeida
Percona Database Performance Blog

Percona Operator for MySQL 1.3.0: autopilot tuning, zero-data-loss async failover, encrypted PITR

  Percona Operator for MySQL 1.3.0 is out. This release moves three things forward for teams running MySQL on Kubernetes: the operator now tunes MySQL for you based on the pod resources, async clusters can fail over without losing data in flight, and point-in-time recovery works on clusters where binary logs are encrypted at rest. … Continued

The post Percona Operator for MySQL 1.3.0: autopilot tuning, zero-data-loss async failover, encrypted PITR appeared first on Percona.

by Slava Sarzhan

October 28, 2026

Percona Database Performance Blog

Why you should stop using ARBITERS in MongoDB

This blog post was born of a discussion with a colleague in Percona Support, who also co-authored it with me here on the use of the ARBITER feature in MongoDB installations nowadays. Turns out, after analyzing past real cases we’ve faced in support, maybe it’s time to say goodbye to ARBITERS. We are not saying … Continued

The post Why you should stop using ARBITERS in MongoDB appeared first on Percona.

by Jean da Silva
Percona Database Performance Blog

How to Extract Data from InnoDB, MyISAM, and MyRocks Files Without a Running Server

Probably everyone responsible for managing database servers at some point realizes that it would be helpful to have a tool capable of extracting data directly from raw database files. Something completely offline, without the need to have a running database server, and that would work with data directories, files, or binary backups (storage volume snapshots, … Continued

The post How to Extract Data from InnoDB, MyISAM, and MyRocks Files Without a Running Server appeared first on Percona.

by Przemysław Malkowski

October 27, 2026

Murat Demirbas

TLA-Verus: LLM agents prove temporal properties of TLA+ specs

This NeurIPS'26 workshop paper takes TLA+ specs from GitHub, translates them into Verus, and has LLM agents prove the safety and liveness properties in the specs.


The motivation

The paper aims to address two problems it raises with TLA+. First, nothing ties the spec to the code, so they drift apart. And second, it claims that proof support is thin: TLC only checks small configurations, and TLAPS is weak on liveness.

They abandon pursuing the first weakness they raise at the onset of the paper. Closing it needs a proof that the generated Rust code (which it turns out TLA-Verus doesn't produce anyway) refines the spec, so they list this as future work. It gets worse though. There is no refinement proof between the TLA+ spec and the Verus spec either. Nothing establishes that the translated Verus spec means what the original meant. (Trace validation, meanwhile, is a viable way of tying TLA+ to implementation code, and has been getting a lot of attention recently.)

They dedicate the paper to addressing the second weakness, but I think they  understate the TLAPS capability for doing temporal proofs. Writing `BY PTL` on a proof step tells TLAPS to treat that step as propositional temporal logic and send it to LS4, an LTL decision procedure. Coalescing (Doligez, Kriener, Lamport, Libal, Merz) is the technique that abstracts the first-order parts of a TLA+ obligation into propositional atoms LS4 can handle. Lamport's temporal proof rules are all there, including WF1, the rule that turns a weak fairness assumption on an action into a leads-to conclusion. The limitation is that TLAPS reasons poorly about ENABLED, and discharging the enabledness side conditions of WF1 is where a liveness proof needs more work. All this to say, TLAPS has temporal proof capability, and last time I used Claude Code to write TLAPS proofs, I was surprised by how well Opus was able to write TLAPS proofs. I expected the paper to compare against TLAPS proofs, but unfortunately that is missing.

Verus, the Rust verifier, is really cool though. It can host temporal logic. It is auto-active, which is the middle ground between a model checker you push a button on and a proof assistant like Coq or Lean you drive yourself. Here you annotate the program with preconditions, invariants, and lemmas, and an SMT solver discharges the resulting obligations automatically. So instead of writing a proof, your job (or more like your LLM's job) is to figure out which hint the solver is missing. Anvil (OSDI'24) demonstrated this capability by proving liveness of Kubernetes controllers, and it did so by building temporal logic as a Verus library, since Verus itself knows nothing about [] and <>. This paper takes that library almost directly to use `always`, `eventually`, `leads_to`, weak fairness, and pre-proven lemmas like WF1. The game plan of the paper is to move the TLA+ spec into Verus, prove things there leveraging Anvil, and later (in the long term plan) prove that the Rust code written refines the proven Verus `spec`.

Some background on Verus is in order here. A Verus file holds three kinds of code. `spec` code is mathematics: it never runs, and it can use unbounded integers and infinite sets. `proof` code is ghost code, lemmas that exist during verification and are erased afterward. `exec` code is real Rust that compiles and ships, and its preconditions and postconditions are written in terms of the `spec` functions. All three live in one file to keep the specification from drifting away from the implementation.

In this paper there is no `exec` code. Every task is `spec` and `proof` only. The translated TLA+ state machine is a `spec` function relating one state to the next, and what the LLM fills in is an empty `proof fn`. Nothing here compiles to a binary executable code. So the distinguishing feature of Verus from other SMT-backed provers is turned off for the entire corpus. Frankly, I can't see how code generation for a distributed system could be made from `spec` automatically even with LLMs.


The pipeline

OK, I got carried away with the motivation and went into too much detail already. Let's backup and checkout the pipeline. The paper's main contribution is the prover-reviewer loop, which is a way to get LLMs to prove temporal properties of TLA+ specs. The pipeline has three stages: translation, proof search, and merge control.

The unit of work throughout is a (spec, property) pair: that is a whole TLA+ specification together with a single property to prove about it. Each pair becomes its own self-contained Verus file carrying exactly one open proof obligation. (Me thinks this is not a sustainable way to generate code from a real system.) Since a module usually declares several properties, pairs provide an inflated way to count: the 16,459 pairs come from only 2,734 TLA+ modules in 838 GitHub repositories, a median of 5 properties per module. The same specification gets translated and proved over and over, once per property.

Translation comes in two flavors. TranSpec is a deterministic Rust transpiler. It infers types for untyped TLA+, synthesizes termination measures, and places SMT triggers. The other flavor is an LLM translator checked by an LLM judge, without any proof for the translation.

Proof search uses a prover agent and a reviewer agent with fresh context. Verus only says which assertion failed, but gives no counterexample, so the reviewer agent supplies the semantic feedback.

A gatekeeper controls the merges, a signed append-only ledger, and a git hook. Anti-cheat checks reject any net-new `assume`, `admit`, or `external_body`. The prover cannot merge its own work. This prevents the proof agent from reward hacking.


The corpus

The paper runs three separate experiments. The first is the full corpus sweep via the prover-reviewer pipeline, driven by Opus. They tried 16,459 (spec, property) pairs. TranSpec translated 6,070 and 5,160 were well-posed. The prover closed 3,094 of those. Liveness was the weakest type: 304 of 809, about 38%. Proofs cost about $2 each. On the agentic side the losses move to a different stage: 2,851 pairs are judged unprovable by an LLM and dropped, with nothing checking that verdict.

The surviving corpus is lopsided. The paper splits safety into three buckets. "Invariance" is a plain state invariant: []P for a state predicate P. "TypeOK" is the type-correctness invariant, pulled out separately. "Safety" category is reserved for everything that is not a single state predicate. Of the 5,160 well-posed algorithmic tasks, invariance and TypeOK together are 83%, liveness is 809 tasks or 16%, and that last "safety" bucket is 50 tasks, 1%. Safety is scarce because TranSpec is bad at those forms rather than because GitHub lacks them: of the 630 safety properties the agentic pipeline translated, 578 have no usable algorithmic bundle at all.


The benchmark

The third experiment drops the reviewer and the gatekeeper. A model gets the task file and runs Verus, up to 10 attempts. So the prover-reviewer loop, the paper's most interesting contribution, is absent from every number in the model table.

The set is 40 tasks, 10 of each property type, in both encodings, and eleven models at pass@3. Opus-5 and GPT-5.6-sol-pro solve everything; gpt-oss-120b solves nothing. Nine of eleven do worse than on verusbench, DeepSeek-R1 falling from 74.7% to 17.5%. Liveness is again the hardest type: models solved 58 of 110 liveness attempts, against 73 to 78 for each of the other three types.

That 53% on liveness looks better than the 38% from the corpus sweep, but the two are not the same question. The second of seven selection criteria is that the task be "known provable", so the 40 tasks are drawn from the 3,094 the prover already closed. The ten liveness tasks come out of the 304 successes, never the 809 attempts. Which is also why the top of the table saturates: Opus-5 scores 100% on a set filtered by what Opus-5 could prove.

I think the task generator is really the useful thing here. Normally a person has to construct/curate a usable/challenging task, which is why verusbench has only 150 tasks. Here Verus decides it. In TLA-Verus, a translation is kept only if it compiles and verifies with exactly one error, the open proof obligation. Zero errors means the property was already true with an empty proof, so there is nothing to prove (145 such tasks were dropped). Two or more errors mean the translation is broken. That said, this check also has drawbacks. Compiling with one error says the file is well-formed Verus with a proof obligation pending, but it does not guarantee that a proof is possible. The property may be false in the original spec, or the translation may have made it false, and then the prover just burns tokens only to record this task as unproven. The paper admits this type of impossible proof is indistinguishable from a proof that was merely hard. The opposite case is worse still: if the translation breaks the state machine instead of the property, the property holds for free and the proof is easy. That is shown in Appendix C.2: their vacuity filter misses it, because that filter only catches tasks that verify with an empty proof. But this may not be a big problem, because these specs come from GitHub and most were model-checked by their authors before being committed, so the properties would be "mostly" true.

by Murat (noreply@blogger.com)
Stack - Convex Blog

Your database is lying to you about time

Date.now() in a Convex mutation isn't actually now, and _creationTime doesn't follow the order things were committed in. Ian sat me down at a whiteboard to explain the three times in a database, how you can miss rows, and how commit timestamps fix it.
by Stack
Database Architects

The Benchmarking Crisis

Goodhart’s law, that any measurable target stops being useful when people start optimizing for it, very much holds in database benchmarking. That is not new, of course. Famously, TPC-D got retired when people optimized so much for it that the query runtimes converged towards zero due to excessive caching. TPC-H fixed that by declaring itself to be an ad-hoc benchmark, and explicitly forbidding things like exploiting knowledge about the workload or caching results (and a number of other optimizations).

We now see the same problem with the ClickBench benchmark, heavily accelerated by today’s use of AI code generation. If you tell an AI to make the queries faster, it will make the queries faster, regardless of whether this is a generally plausible approach or not. For example, the pgrust implementation performs group-by aggregations on string columns purely on the hash value, ignoring the long string content. That is a great performance boost, of course, and works for this benchmark, but can produce wrong results. Is it faster? Yes. Is it a plausible optimization? Probably not. And it does many other things: For example, ClickBench repeats certain predicates across queries, and thus pgrust caches the predicate, completely eliminating the query cost the second time. Or for query Q17, which returns tuples grouped by userid, it makes use of the fact that a) tuples are roughly clustered by userid, and b) the query specifies a limit clause without order by. Thus any userid will do, and it never reads most of the data. A human would not do these tiny micro-optimizations, because they are unlikely to be relevant in general use cases, but an AI can of course look at each query in detail and tune for it.

Part of the problem is, of course, ClickBench itself. The benchmark is not well specified in what is permitted and what is not, there is no update stream, the queries are very simple, share predicates, are underspecified, etc. But the fundamental problem is independent of that concrete benchmark: The moment we start aggressively optimizing for a specific benchmark, the benchmark stops being very useful. Historically, that pressure was reduced a bit by the requirement that systems be generally useful. That is, they did not just want to perform well in benchmarks but also to be useful for their customers. That is, of course, not a concern for vibe-coded execution engines.

It is not clear what to do about it. Our SQLStorm proposal tried to address this by having tens of thousands of queries, which makes overfitting harder. No human would fine-tune their system to such a huge workload. But with AI tools we could even investigate ten thousand queries in detail if needed, so that is not a real defense.

I think that to be meaningful, a benchmark has to a) like TPC-H, be ad-hoc, and forbid exploiting prior knowledge and any form of intermediate result caching. If we don’t do that, execution times converge towards zero. And b) the benchmark has to include some form of update stream, as otherwise overly aggressive read-only or read-mostly systems will always outperform systems that offer full transactional support. And c) the benchmark has to be truly ad-hoc, in the sense that the systems tested have to be older than the benchmark. One way to fight Goodhart’s law would be to (automatically) come up with a new benchmark from time to time, and then measure the systems that existed before the benchmark. The caching/pre-computation problem still remains, of course, but at least that would prevent the over-aggressive adjustment to just one specific benchmark.

Interestingly, the machine learning community has struggled with exactly the same problem for years, and we should probably borrow some of their ideas. Kaggle competitions, for example, rank submissions on a hidden test set that participants never see, which makes overfitting on the public data pointless. Similarly, benchmarks like LiveBench regularly release new questions to make sure that models cannot have seen them during training. For database benchmarking that could mean keeping the actual benchmark queries secret and only publishing a representative sample for development, or, even better, generating a fresh workload for every evaluation round. SQLStorm already uses generated queries, so producing a new query set from time to time would be fairly easy. We would probably want a more generic approach (higher variety in schemas, update streams, transactions, etc.), but that seems to be a direction that would help keep benchmarks meaningful.

by Thomas Neumann (noreply@blogger.com)
PlanetScale Blog

What was the turning point for Postgres?

Postgres is the most popular database choice among developers. Postgres is the default choice for agents, powering countless applications where those new to app building don't even know what a database is. Every major cloud offers hosted Postgres.
by Simeon Griggs