Logos: Certified Order-Sensitive SQL Rewrites with Mechanized Semantics and LLM Guidance

Jing-Yu Ke, Jingyang Li, Guoqiang Li. 2026.

What this paper does with SQLancer

One citation in threats to validity, noting that tools such as NoREC expose optimizer bugs by constructing differential or metamorphic oracles -- the empirical counterpart to what Logos proves. Logos verifies SQL rewrite equivalence in the Rocq proof assistant. The authors mechanise a compositional logical semantics for a typed SQL core with order-sensitive operators, capturing all possible ordered lists and observable failures, which they describe as the first mechanised SQL semantics combining nested tie-sensitive top-k with a lifting from bag equivalence to ordered-list equivalence. Logos then uses an LLM-guided agent with a verified lemma library, solving 86.9% of 389 query pairs against 64.0% for the strongest baseline. Written by claude-opus-5 from the 1 place this paper refers to SQLancer. The quotations below are the paper's own words, stored verbatim when the text was extracted.

How it was classified

uses infrastructure — no

SQLancer is cited, not used; nothing in the mentions describes reusing its code.

extends technique — no

No technique is extended; the citation is background.

compares with — no

No empirical comparison against SQLancer is reported in the mentions.

describes as state of the art — no

The citation does not characterise SQLancer as the state of the art.

SQLancer publications it cites (1)

Bibliography entries that resolved to a SQLancer publication, or to a paper by one of the project's authors. A sentence citing one of these numbers is a reference to SQLancer even when it never writes the name.

#	Entry	Matched as
19	Manuel Rigger and Zhendong Su. 2020. Detecting Optimization Bugs in Database Engines via Non-Optimizing Reference Engine Construction. InProceedings of the 28th ACM Joint Meeting on European Software Engineering Confe...	sqlancer publication · NOREC

Every place it refers to SQLancer (1)

1 sentence, each stored verbatim from the extracted text with where it was found and how. “Citation marker” means the sentence names no tool at all and was reached through a reference number that resolved to a SQLancer publication.

Id	Sentence	Found by	Where
M1	Testing and fuzzing tools such as NoREC expose optimizer bugs by constructing differential or metamorphic test oracles [ 19].	technique background	5.4 Threats to Validity page 12

This page is rendered from _data/papers/paper_arxiv_2608_15709.json, extracted from arxiv. 13 pages, 30 references parsed.