What it is
Synthesizes workload-specific Rust database engines from SQL and formally verifies them with Verus. Reported speedups reach 61.3× over DuckDB and 28.3× over Umbra. Generate a workload- and hardware-specific database engine from SQL, then prove the produced Rust crate returns correct answers and is memory-, arithmetic-, and race-safe.
Key results
- Up to 61.3× over DuckDB and 28.3× over Umbra on SEC-EDGAR
- 51.6× over DuckDB and 22.0× over Umbra on TPC-H 22 queries
- Verus proves correctness, memory safety, arithmetic safety, no data races
Shows AI can synthesize database engines that are both formally verified and substantially faster than mature systems on targeted workloads.