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

Jingyu Ke, Jingyang Li, Guoqiang Li

SQL rewrite verification must account for duplicate rows, observable row order, and typed value semantics. Existing verifiers have yet to combine proofs over database instances of…