Both optimizations avoid (skip) reading (scan) irrelevant leaf pages by repositioning (seek) via a fresh index descent instead of scanning sequentially. This surface similarity explains why people often used "skip scan" and "loose index scan" interchangeably before the distinction was clearly defined. For example, I wrote YugabyteDB Skip Scan aka Loose Index Scan on compound index in 2022 because the two concepts were not clearly distinguished in the PostgreSQL wiki at that time. PostgreSQL implemented neither of those features yet, and YugabyteDB implemented both with the same hybrid scan mechanism. However, today the distinction matters because PostgreSQL 18 has added Skip Scan but not Loose Index Scan.
A plain range scan seeks once to the start of a range and then reads forward or backward until past the end. Both Skip Scan and Loose Index Scan can instead reposition to a new range, or "grouping" (a run of index entries sharing the same leading-column value), via a new index descent, rather than reading through a single range sequentially. This avoids reading irrelevant leaf pages.
Skip Scan avoids reading leaf pages entirely outside a relevant sub-range. PostgreSQL does not skip index entries that might match: within a grouping, it still examines the relevant entries and returns every match, exactly as a normal scan would within that sub-range. Separately, PostgreSQL can sometimes avoid rechecking a scan key on a page whose high key proves that all entries satisfy it (as a CPU optimization), but it does not avoid reading the page.
A Loose Index Scan, by contrast, deliberately reads only the first entry of each range and then jumps to the next range — it never reads the remaining matching rows because it isn't trying to satisfy a later-column predicate, only to enumerate the distinct values of a prefix.
In short:
| Skip Scan | Loose Index Scan | |
|---|---|---|
| Skips | Leaf pages belonging to sub-ranges that can't satisfy the later-column predicate | Leaf pages/entries belonging to any range after its first entry |
| Within a matched range | Reads/checks every entry against the later-column | Reads one entry, then repositions to the next range |
| Purpose of the leading column | Vehicle for enumerating candidate ranges so a later-column predicate can be applied efficiently | The thing being enumerated (e.g., DISTINCT) — no later-column predicate needed |
Both optimizations benefit when the leading index column has relatively few distinct values and many rows per value. Repeated descents are then cheaper than scanning large groups of entries sequentially.
Skip Scan may be rejected when the number of descents exceeds the cost of scanning the index normally. A Loose Index Scan has the same trade-off: if almost every row has a different prefix value, one descent per value is not worthwhile. Its advantage appears when each group contains enough duplicate entries to make skipping the rest of the group profitable.
The distinction is therefore not primarily the index definition or the data distribution. It is the query's objective: Skip Scan must return all matching rows, whereas Loose Index Scan deliberately returns only one representative per group.
I created a table with an index on two columns:
CREATE EXTENSION IF NOT EXISTS pageinspect;
DROP TABLE IF EXISTS demo CASCADE;
CREATE TABLE demo (
a integer NOT NULL,
b text NOT NULL,
payload text NOT NULL
);
INSERT INTO demo (a, b, payload)
SELECT
a,
repeat(md5(g::text), 28), -- approximately 900 bytes
repeat('payload-' || a || '-' || g, 20)
FROM generate_series(1, 8) AS a
CROSS JOIN generate_series(1, 80) AS g;
CREATE INDEX demo_ab_idx ON demo (a, b);
VACUUM ANALYZE demo;
Here is a query that shows the index entries in their logical order:
SELECT
s.blkno AS index_block,
i.itemoffset,
d.a,
left(d.b, 100) || '...' AS b,
i.itemlen,
i.htid,
i.data as data
FROM bt_multi_page_stats('demo_ab_idx', 1, -1) AS s
CROSS JOIN LATERAL bt_page_items('demo_ab_idx', s.blkno) AS i
JOIN demo AS d
ON d.ctid = i.htid
WHERE s.type = 'l'
ORDER BY
d.a,
d.b;
A Skip Scan will scan all values of "a" but may skip the portions of each "a" grouping outside the "b" range, for example WHERE b LIKE '28%':
index_block | itemoffset | a | b | itemlen | htid | data
-------------+------------+---+---------------------------------------------------------------------------------------------------------+---------+---------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
1 | 14 | 1 | 2838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838... | 72 | (8,2) | 01 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 33 38 30 32 33 61 37 37 38 64 66 61 65 63 64 63 32 31 32 37 30 38 66 37 32 31 62 37 38 38 20 00 ff ff ff 4b 50 31 62 37 38 38 00 00 00 00 00 00
1 | 15 | 1 | 28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd... | 72 | (12,4) | 01 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 64 64 32 63 37 39 35 35 63 65 39 32 36 34 35 36 32 34 30 62 32 66 66 30 31 30 30 62 64 65 20 00 ff ff ff 4b 50 30 30 62 64 65 00 00 00 00 00 00
1 | 94 | 2 | 2838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838... | 72 | (21,3) | 02 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 33 38 30 32 33 61 37 37 38 64 66 61 65 63 64 63 32 31 32 37 30 38 66 37 32 31 62 37 38 38 20 00 ff ff ff 4b 50 31 62 37 38 38 00 00 00 00 00 00
1 | 95 | 2 | 28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd... | 72 | (25,5) | 02 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 64 64 32 63 37 39 35 35 63 65 39 32 36 34 35 36 32 34 30 62 32 66 66 30 31 30 30 62 64 65 20 00 ff ff ff 4b 50 30 30 62 64 65 00 00 00 00 00 00
2 | 78 | 3 | 2838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838... | 72 | (34,3) | 03 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 33 38 30 32 33 61 37 37 38 64 66 61 65 63 64 63 32 31 32 37 30 38 66 37 32 31 62 37 38 38 20 00 ff ff ff 4b 50 31 62 37 38 38 00 00 00 00 00 00
2 | 79 | 3 | 28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd... | 72 | (38,5) | 03 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 64 64 32 63 37 39 35 35 63 65 39 32 36 34 35 36 32 34 30 62 32 66 66 30 31 30 30 62 64 65 20 00 ff ff ff 4b 50 30 30 62 64 65 00 00 00 00 00 00
4 | 62 | 4 | 2838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838... | 72 | (47,3) | 04 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 33 38 30 32 33 61 37 37 38 64 66 61 65 63 64 63 32 31 32 37 30 38 66 37 32 31 62 37 38 38 20 00 ff ff ff 4b 50 31 62 37 38 38 00 00 00 00 00 00
4 | 63 | 4 | 28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd... | 72 | (51,5) | 04 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 64 64 32 63 37 39 35 35 63 65 39 32 36 34 35 36 32 34 30 62 32 66 66 30 31 30 30 62 64 65 20 00 ff ff ff 4b 50 30 30 62 64 65 00 00 00 00 00 00
5 | 46 | 5 | 2838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838... | 72 | (60,3) | 05 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 33 38 30 32 33 61 37 37 38 64 66 61 65 63 64 63 32 31 32 37 30 38 66 37 32 31 62 37 38 38 20 00 ff ff ff 4b 50 31 62 37 38 38 00 00 00 00 00 00
5 | 47 | 5 | 28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd... | 72 | (64,5) | 05 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 64 64 32 63 37 39 35 35 63 65 39 32 36 34 35 36 32 34 30 62 32 66 66 30 31 30 30 62 64 65 20 00 ff ff ff 4b 50 30 30 62 64 65 00 00 00 00 00 00
6 | 30 | 6 | 2838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838... | 72 | (73,3) | 06 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 33 38 30 32 33 61 37 37 38 64 66 61 65 63 64 63 32 31 32 37 30 38 66 37 32 31 62 37 38 38 20 00 ff ff ff 4b 50 31 62 37 38 38 00 00 00 00 00 00
6 | 31 | 6 | 28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd... | 72 | (77,5) | 06 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 64 64 32 63 37 39 35 35 63 65 39 32 36 34 35 36 32 34 30 62 32 66 66 30 31 30 30 62 64 65 20 00 ff ff ff 4b 50 30 30 62 64 65 00 00 00 00 00 00
7 | 14 | 7 | 2838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838... | 72 | (86,3) | 07 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 33 38 30 32 33 61 37 37 38 64 66 61 65 63 64 63 32 31 32 37 30 38 66 37 32 31 62 37 38 38 20 00 ff ff ff 4b 50 31 62 37 38 38 00 00 00 00 00 00
7 | 15 | 7 | 28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd... | 72 | (90,5) | 07 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 64 64 32 63 37 39 35 35 63 65 39 32 36 34 35 36 32 34 30 62 32 66 66 30 31 30 30 62 64 65 20 00 ff ff ff 4b 50 30 30 62 64 65 00 00 00 00 00 00
7 | 94 | 8 | 2838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838023a778dfaecdc212708f721b7882838... | 72 | (99,3) | 08 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 33 38 30 32 33 61 37 37 38 64 66 61 65 63 64 63 32 31 32 37 30 38 66 37 32 31 62 37 38 38 20 00 ff ff ff 4b 50 31 62 37 38 38 00 00 00 00 00 00
7 | 95 | 8 | 28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd2c7955ce926456240b2ff0100bde28dd... | 72 | (103,5) | 08 00 00 00 da 00 00 00 80 03 00 40 ff 11 32 38 64 64 32 63 37 39 35 35 63 65 39 32 36 34 35 36 32 34 30 62 32 66 66 30 31 30 30 62 64 65 20 00 ff ff ff 4b 50 30 30 62 64 65 00 00 00 00 00 00
A Loose Index Scan will read only the first row for each value of "a", for example, in SELECT DISTINCT ON (a):
index_block | itemoffset | a | b | itemlen | htid | data
-------------+------------+---+---------------------------------------------------------------------------------------------------------+---------+--------+-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
1 | 2 | 1 | 02e74f10e0327ad868d138f2b4fdd6f002e74f10e0327ad868d138f2b4fdd6f002e74f10e0327ad868d138f2b4fdd6f002e7... | 72 | (4,2) | 01 00 00 00 da 00 00 00 80 03 00 40 ff 11 30 32 65 37 34 66 31 30 65 30 33 32 37 61 64 38 36 38 64 31 33 38 66 32 62 34 66 64 64 36 66 30 20 00 ff ff ff 4b 50 64 64 36 66 30 00 00 00 00 00 00
1 | 82 | 2 | 02e74f10e0327ad868d138f2b4fdd6f002e74f10e0327ad868d138f2b4fdd6f002e74f10e0327ad868d138f2b4fdd6f002e7... | 72 | (17,3) | 02 00 00 00 da 00 00 00 80 03 00 40 ff 11 30 32 65 37 34 66 31 30 65 30 33 32 37 61 64 38 36 38 64 31 33 38 66 32 62 34 66 64 64 36 66 30 20 00 ff ff ff 4b 50 64 64 36 66 30 00 00 00 00 00 00
2 | 66 | 3 | 02e74f10e0327ad868d138f2b4fdd6f002e74f10e0327ad868d138f2b4fdd6f002e74f10e0327ad868d138f2b4fdd6f002e7... | 72 | (30,3) | 03 00 00 00 da 00 00 00 80 03 00 40 ff 11 30 32 65 37 34 66 31 30 65 30 33 32 37 61 64 38 36 38 64 31 33 38 66 32 62 34 66 64 64 36 66 30 20 00 ff ff ff 4b 50 64 64 36 66 30 00 00 00 00 00 00
4 | 50 | 4 | 02e74f10e0327ad868d138f2b4fdd6f002e74f10e0327ad868d138f2b4fdd6f002e74f10e0327ad868d138f2b4fdd6f002e7... | 72 | (43,3) | 04 00 00 00 da 00 00 00 80 03 00 40 ff 11 30 32 65 37 34 66 31 30 65 30 33 32 37 61 64 38 36 38 64 31 33 38 66 32 62 34 66 64 64 36 66 30 20 00 ff ff ff 4b 50 64 64 36 66 30 00 00 00 00 00 00
5 | 34 | 5 | 02e74f10e0327ad868d138f2b4fdd6f002e74f10e0327ad868d138f2b4fdd6f002e74f10e0327ad868d138f2b4fdd6f002e7... | 72 | (56,3) | 05 00 00
Percona University Comes to Uruguay
Percona University is coming to Montevideo. On September 23rd, 2026, we’re getting together for a full day of technical talks on open source software, and you are invited! If you work or study with open source software in Uruguay, this one is for you. It’s a whole day of learning, with the people who build … Continued
The post Percona University Comes to Uruguay appeared first on Percona.
What is a data topology?
A data topology describes the sharding scheme a Neki router uses to map logical PostgreSQL tables to physical shards and route queries.
MVCC not only tracks row history but also records the search-key space. To better understand PostgreSQL MVCC, it's useful to look at some alternatives. One is zheap, which introduced out-of-place undo logging to rebuild historical row versions by storing old tuples in an undo log instead of the heap. This was done entirely at the table access method level, without modifying the index access method, but it was eventually abandoned. A more recent development is OrioleDB, which extends this approach to cover the search-key space with an MVCC index access method. Due to PostgreSQL's extensive ecosystem that supports multiple index types such as hash, GIN, BRIN, SPGiST, and others through extensions, OrioleDB uses a "bridge index" to ensure compatibility.
OrioleDB is a PostgreSQL table access method that replaces the ordinary heap with index-organized, version-aware B-trees. Complete rows are stored in the primary B-tree. Native secondary indexes store the secondary key plus the primary key, allowing them to point back to the complete row.
That layout is easy to compare with InnoDB's clustered index, but the key difference is not clustering. It is how OrioleDB preserves old snapshots as rows, keys, and B-tree pages change. OrioleDB keeps two kinds of history:
The second kind is what makes OrioleDB architecturally interesting. MVCC must preserve not only what a row used to contain but also where an old query would have found it.
Suppose an old snapshot is open while another transaction modifies an order:
UPDATE orders
SET status = 'closed'
WHERE order_id = 42;
Before the update, a secondary index contains an entry conceptually like ('open', 42). Afterward, the current tree contains ('closed', 42).
Row undo can reconstruct the old value status = 'open' after row 42 has been found. It cannot scan the old open range to find row 42. The current secondary B-tree routes the row under closed.
An MVCC engine must therefore solve two distinct problems:
| Problem | Question |
|---|---|
| Payload visibility | Which version of row 42 may this snapshot read? |
| Predicate reachability | Should a scan of status = 'open' enumerate row 42? |
PostgreSQL solves reachability by retaining old heap tuples and old index entries until VACUUM can safely remove them. InnoDB retains old secondary records as delete-marked entries until purge. OrioleDB's native indexes instead use page-level undo to reconstruct the historical searchable key space.
The primary B-tree stores complete rows. Its key is the table's primary key, or an internal key if no primary key is defined. A native secondary leaf stores the secondary key and primary key rather than a PostgreSQL heap TID.
A secondary lookup therefore follows this path from the secondary key:
Both trees participate in snapshot visibility. A secondary index is not merely a current-key candidate generator whose result can always be repaired at the primary row. It must first enumerate the keys that were part of the requested snapshot.
This tight integration has both benefits and costs. OrioleDB can make its native indexes understand its version model directly. However, PostgreSQL index access methods such as GiST, GIN, SP-GiST, BRIN, hash, and any new index type brought by a PostgreSQL extension do not understand OrioleDB primary keys or undo.
OrioleDB supports those methods through bridge indexes. An ordinary index stores a synthetic heap-shaped bridge_ctid. An internal OrioleDB bridge tree maps that identifier to the primary key. This preserves PostgreSQL's index-AM extensibility but adds an extra lookup and reintroduces stale index entries and a VACUUM cleanup cycle into the design. Native and bridged indexes therefore have different maintenance contracts.
A secondary lookup from such indexes now follows this path:
bridge_ctid
Row-level undo maintains a tuple's history. It records enough information to select or reconstruct the row version visible at a snapshot. The same undo machinery also supports transaction rollback.
Page-level undo records changes to B-tree leaves. It covers ordinary changes, such as insertions and deletions, as well as physical maintenance, such as compaction, splits, and merges. These operations can move keys or change page boundaries, even when their purpose is only to keep the current tree balanced.
That distinction matters during a range scan. A page split may move an old key onto a page that did not exist at the snapshot. A merge may erase the boundary that an old scan needs. OrioleDB can reconstruct a historical page image and, where necessary, merge historical and live items while preserving order and avoiding omissions or duplicates.
The conceptual read path for the example is:
Page undo answers why the scan finds the row. Row undo answers what the row contained.
In PostgreSQL, a B-tree split is primarily a physical index operation. Historical membership persists because old index tuples still point to old heap tuples. The index does not need to preserve the old page topology for snapshot reads.
In OrioleDB, a split also changes the partitioning of the searchable key space. Compaction, merge, and page reuse carry the same additional obligation. A page cannot be treated as irrelevant merely because it is obsolete in the current tree. Retained snapshots may still need its earlier contents or boundaries.
This moves work rather than eliminating it:
snapshot too old boundaryA single logical update can modify the primary tree and several secondaries. Current OrioleDB tracks the short primary-applied, secondary-pending interval to prevent a checkpoint from permanently merging mismatched tree states. Recovery starts from a copy-on-write checkpoint, replays row-level WAL, repairs derived secondary work as needed, and rolls back incomplete transactions.
The engines below often use similar words while assigning history to different structures:
| Engine | Current organization | How old indexed membership survives | Principal deferred cost |
|---|---|---|---|
| PostgreSQL | Heap tuples plus separate indexes | Old index entries continue to reference old version TIDs | Heap and index VACUUM, freezing, and bloat control |
| OrioleDB native | Complete rows in primary B-tree. Secondaries carry primary keys | Page undo reconstructs historical leaf items and ranges | Undo retention, reconstruction, and tree-aware reclamation |
| OrioleDB bridged | Native primary plus synthetic identities in ordinary index AMs | External entries plus a versioned bridge mapping | Extra lookups and bridge-aware VACUUM
|
| Oracle Database | Heap blocks, indexes, undo, and consistent-read block images | Transactional index changes and undo/CR preserve logical visibility | Undo retention and optional physical coalesce/rebuild |
| InnoDB | Clustered primary plus secondary B-trees | Old secondary records remain delete-marked until safe purge | Undo history and purge lag |
| WiredTiger | Per-key update chains and reconciled B-tree images | Older key values remain in update chains or the history-store B-tree | Reconciliation, eviction, cache pressure, and history cleanup |
Oracle is similar in that it uses undo to construct a consistent view, but its block formats, index algorithms, and recovery machinery differ. It should not be described as rewinding an old root-to-leaf tree for every query.
WiredTiger is especially useful for comparison because it also keeps version history close to B-tree keys. Its in-memory update chains and history store optimize storage-engine keys. OrioleDB additionally ensures PostgreSQL table and secondary-index consistency across several trees.
Recent research shows that storing versions "in the B-tree" can mean different things.
MV-PBT writes changes to a current memory-resident partition, persists full partitions sequentially, and later merges immutable partitions. Version information in index records enables index-side visibility filtering. It trades OrioleDB-style page reconstruction for cross-partition search and a merge policy closer to LSM storage economics.
The cMVBT preprint represents historical trees explicitly as a partially persistent DAG. Snapshot scans traverse immutable committed nodes without latches, while writers perform proactive version and key splits and merges with optimistic latching. OrioleDB instead maintains a current topology and reconstructs historical leaves from page undo.
cMVBT is a valuable design comparison, not yet a production-engine comparison. Its reported implementation is in-memory, uses fixed-size keys and values, and supports single-operation write transactions. External storage, crash recovery, and arbitrary multi-operation ACID transactions remain outside the scope of that evaluation.
OrioleDB's claim is not just that undo operations are less costly than keeping old heap tuples. Instead, it argues that row undo, page undo, version-aware native B-trees, copy-on-write checkpoints, and row-level WAL can work together more efficiently than PostgreSQL's heap, index, and vacuum system.
The most indicative tests are not just current-key lookups. They include historical snapshots covering indexed-key modifications, long-range scans during split and merge processes, ongoing deletes and space reuse, checkpoint crashes within primary/secondary update windows, and bridged-index workloads with delayed vacuum.
OrioleDB is still a work-in-progress open-source project in beta, requiring a patched version of PostgreSQL. Its source code reflects an ambitious and well-structured architecture rather than a stable core PostgreSQL implementation. The effectiveness of the design should be evaluated based on how well it manages historical key ranges, maintenance, cleanup, and recovery processes under real-world mixed workloads.
The core concept is simple: an old row value is useful only if the old predicate can still locate it. OrioleDB incorporates this requirement directly into the B-tree and uses an additional bridge index to remain compatible with other PostgreSQL index types.
Our first post showed MySQL 9.7 with one change: mark a table ENGINE=DuckDB and its analytical queries run in DuckDB instead of InnoDB. The question we kept getting after that was about replication. Can you keep a normal InnoDB primary for the writes, and run a replica where the big tables are ENGINE=DuckDB? Then the … Continued
The post Replicating from InnoDB into a DuckDB storage engine appeared first on Percona.
Specula is an agentic system that automates the process of software bug finding through authoring and model-checking a spec for the code. It derives TLA+ specifications automatically from the code, checks code-spec conformance through trace validation, model checks the spec to find concurrency bugs, and reproduces the bug at the code layer by writing integration tests with precise timing.
I remember reading the Daikon paper "Quickly detecting relevant program invariants" in 2000 and getting impressed by it, and here we are after 26 years, solving the end-to-end problem much better than I ever thought would be possible in a push-button manner in the year of our lord 2026.
But somehow, I am still somewhat unsatisfied with the paper. This may be me being hypercritical and trying to get more out of the paper by arguing with it. So bare with me until I resolve (or learn to accept) these problems over time. I know many of the authors of the Specula work, and respect them, and I know they won't take my critiques about the larger problem in a wrong way... I am trying to make sense of the terrain myself.
So, let's look at what Specula gets right, its major contributions, and then dive into my unresolved questions and existential thinking about the terrain.
Specula is run on "slices of" 48 complex open-source distributed and concurrent systems including MongoDB, Microsoft's SONiC network OS, GCC's libgomp, Etcd, and RabbitMQ's ra. It found 249 bugs, 207 of them new. The 48 systems span 7 languages, from C to Erlang to Rust. This is very impressive, and it earns the "scaling" claim in the title of the paper. Hand-crafting TLA+ specifications may take weeks (especially for unfamiliar code bases), and Specula completes end-to-end checks in 1.4 to 9.8 hours at a median token cost of $57 per system. Did I mention this is all push-button? Developers just review the end results. They may not even have to look at the TLA+ specs, and they may just check the reported bugs and figure out how to address them.
OK, impressive. Let's dive into the technical novelty here. As far as I understand the technical novelty arises from two opposing forces dueling it out in self-evolving loops, to achieve an "iron sharpens iron" effect. Trace validation pulls the spec toward the code, and model checking pushes back. You need the two opposing forces, because either one alone gets fooled. Left with only trace validation as its reward signal, the agent does reward-hacking: it relaxes guards in the spec, adds wildcards, hardcodes trace-specific updates just to make the log replay. For example, in the Kudu-Raft application, the agent "repairs" the follower's accept path so it overwrites the log suffix unconditionally, and the traces replay beautifully, and then State Machine Safety catches the problem in one step. The model checking checks that the spec/model has nothing illegal in it. Specula wires them into self-evolving loops where each iteration hands the agent new evidence, a counterexample, a model-code gap, a failed reproduction, and forces it to reconsider. In short, these loops turn an unreliable agent into a reliable one.
To evaluate this technical novelty, they ran the same prompts three ways: Claude Code raw, Claude Code with the official TLA+ skills and MCP servers, and Specula. On five systems, Specula finds 62 bugs, raw finds 2, and TLA+-equipped finds only 3. So handing a frontier agent the entire TLA+ toolchain doesn't buy you much, and Specula leaves that baseline in the dust. As the authors put it, what is lacking is not TLA+ knowledge, it is the runtime feedback that lets the agent repair what it wrote. I think that large gap in the evaluation highlights that the technical contribution of Specula is not prompting/hyping LLMs, and is not just handing the LLM a model checker.
But, my problem is that I cannot put my finger on the technical contribution in a very robust/solid/concrete sense. The technical contribution seems to be, so to speak, self-emerging from a set of (somewhat unsound) heuristics. Let me try to explain...
Specula treats system artifacts (code, git commit history, PRs, comments) as the ground truth to derive invariants. 87% of its invariants trace back to the implementation code and comments, 74% to issue trackers, and only 20% to documentation. So the specification derivation sources from the code, the same place the bugs live. So how does Specula find bugs if it treats the codebase as the ground truth? Wouldn't it just copy existing bugs into the model as intended behavior? What stops this?
Leslie Lamport will never understand this... You need a separate requirements spec, and separate code. For formal methods people, writing the specification IS understanding the problem; the code is the easy part afterwards. Specula runs that backwards: the code is the given, and the understanding is reconstructed from it. But then the word "specification" is doing something different than it does in Lamport's world (i.e., formal methods and mathematics), and the paper never talks about this.
This is also where the vocabulary starts sliding. In the conformance loop the paper considers three cases: the model/spec is incorrect, the code has a bug, or the invariant is incorrect. Incorrect with respect to what?? For the model/spec, the answer is with respect to the code, and for the code the answer is with respect to the model/spec. Notice the circularity? For the invariant, there is no external reference point at all! The invariant is incorrect with respect to the agent's own reading of the artifacts, revised by the agent, justified by evidence the agent selects.
The practical answer the paper offers, as far as I can tell, is that specification will identify a bug when the artifacts disagree with each other. Specula's scenario generation tries to catch these disaggrements. But, if the design is wrong and everybody wrote it down consistently, there is nothing to catch. If the agent misreads an ambiguous comment in the other direction, it would quietly relax a real invariant to match a code flaw, and you never hear about it.
They ran all of this on an Azure VM with a 96-core AMD EPYC 9V74 and 384GB of RAM, driving Claude Code with Opus-4.8 at a 1M context and max reasoning. And even with that machine, Specula does not model check the full reference specification, because it would blow up the state space. Instead, it projects things down to the aforementioned per-scenario models with some tricks: bound how many times an action can fire, (e.g., bound=0 for a crash action means happy path checking), coarsen multi-step processes into one atomic action, and serialize action pairs into a fixed order.
Every one of these is a legitimate technique, and human modelers use all three. What bothers me is that none of it is justified. Why these three operations? Coarsening an action is only sound for properties that do not observe the intermediate states, so which invariants survive which coarsening? The paper says intermediate states are abstracted out and moves on. When a human expert makes that call they have a justification in mind. I am not sure about agents trying these in an automated way. It sounds more ad hoc, as a means for smart fuzzing the system.
The protocol-level versus code-level split has the same feel, and I think it is more critical because it is load-bearing. The whole anti-reward-hacking argument depends on protocol-level invariants being independent of the code the agent just modeled. The paper gives example: Etcd-Raft gets "committed entries are on durable storage," but MongoDB gets the weaker "an entry is in the server's own log before it is reported committed," because MongoDB deliberately deviates from Raft to cut write latency, and the agent digs that out of the revision history. Nice. So protocol-level means it holds for any conforming implementation, and code-level means it is what this implementation promises. Except only 21.1% of Specula's invariants are protocol-level. The other 78.9% are code-level, mined from the same artifacts as the model. So the guard against overfitting rests on a fifth of the invariants, and the agent is the one who decides which fifth, and nothing checks that call. Misclassify a description of the current code as a protocol-level invariant, and you are now guarding against reward hacking using a reward-hacked artifact. This is in essence a sharper version of my complaint about spec from code being circular. What worries me further is by looking at Fig 3.a and 3.b, I don't see any structural or qualitative difference between the two invariant types, so the distinction seems more ad hoc and easy to blur/confuse.
Then there is the convergence issue. The paper says the evolving loops are safe and that Specula "offers convergence with the assumption that agents improve over the iterations". That is not assuring because the assumption does all the work. The stated failure mode of a bad invariant is that the process just does not converge and keeps iterating, and in practice you stop it with a time or token budget. Their numbers are better than I expected, all recorded runs converged, instrumentation fixed within three rounds, 91.3% of invariant and model errors fixed in one iteration, none over four. The one case that needed four rounds was SONiC's link manager. The agent wrote an invariant saying a link's two gateways are never both on standby. Model checking kept finding states where they both are: a failover in mid-handoff, or a degraded mode where neither gateway can take over. Those states are legal, just temporary. It took four counterexamples before the agent stopped calling them bugs and fixed its invariant instead. So the self-evolving loop worked once again. But, this also shows how hard it is to tell a real bug from a state that only looks broken.
I mean it is all pragmatic, which is fine. But I am really bugged by lack of principled justification for these. And the ad hocness of their introduction/descriptions in the paper. Maybe this is the new science we are doing... A more heuristic type of computer science with a mix of anthropology (well, study of agents, so agentology). Maybe in the future, the paper's will consists mostly of field notes on how agents misbehave and which guardrails stop them.
No denying to it, Opus does a lot of the heavy lifting in Specula, and the authors are upfront about it. Swap in Sonnet-4.6 and Specula finds only 10 of those 62 bugs, at nearly the same wall clock and 61% of the cost, so $59 per bug instead of $16. Swap in Haiku-4.5 and it finds nothing at all, and keeps declaring the task done before it is done. The gap shows up in the spec-quality scores: Haiku still writes 95% correct TLA+ syntax, but scores 17% on invariants. But look at how fast that part moved. When I reviewed SysMoBench, the benchmark from this same group (which came on Jan 2026), the authors had handed LLMs invariant templates and asked it only to map them onto its own variable names, because invariants are the most signal-heavy part of a spec. Specula now has agents deriving invariants from commit history unaided.
Specula is a great pragmatic idea, and it works for what it does. My critiques are mostly about naming the contributions/mechanisms more precisely, plus a last ditch effort to get the ad hocness out of the methods. And I should be honest about where that effort is coming from. When we get around to writing our own paper on agentic specification-based development, I am certain we will reach for the same kind of heuristics, and I will find myself defending them with the same hand-waving I am complaining about here. That is what is really bugging me. I do not know what the non-ad-hoc version of this paper would even look like.
All this being said, there is still plenty is to address even on the pragmatic front, because Specula skirts the real hard problem: composition. Specula steers away from authoring and reasoning with compositional specs for multi-service codebases. There is no compositional verification or assume-guarantee reasoning employed when writing specs, as they are monolithic cross-slices of a system. For a system with multiple services, like SONiC's 5 distinct daemons, Specula builds one model per module and mocks the cross-service interactions inside the scenario models. So it cannot say anything about whether the per-module guarantees add up to a system-level guarantee. Unfortunately, the failures you actually fear in distributed systems are the cross-boundary ones, especially for recovery related failures.
PS1: TLA+ for the win!! I got so wrapped up in my own thinking around Specula that I forgot to pat TLA+ on the back. Full disclosure, I am part of the TLA+ Foundation, which recognized and provided some funding for Specula. It is a great addition to the TLA+ ecosystem, and you should go try it: https://github.com/specula-org/Specula
PS2: Here is the link to my marked up copy of the paper. Even with the availability of LLMs, I still believe in deep manual reading, and illustrating one's thought-processes to teach/train others.
We’re happy to announce that Percona Server for MongoDB (PSMDB) 8.0.28-12 extends platform support to RHEL 10 and its derivatives (Oracle Linux 10, Rocky Linux 10, AlmaLinux 10, and other RHEL-compatible distributions) for both x86_64 and ARM (aarch64) architectures. This release also adds support for Debian 13 “Trixie” on x86_64 and ARM64. We’ll continue to … Continued
The post Percona for MongoDB: RHEL 10, Its Derivatives, and Debian 13 – On Both x86_64 and ARM appeared first on Percona.