Show notes
Shu Liu, Alexander Krentsel, Mert Cemri, and Shubham Agarwal, PhD students at U.C. Berkeley's Sky Computing Lab, join the Weaviate Podcast to discuss SkyDiscover and what it means for AI to build entire systems, not just code! AI coding went from Copilot-style line completion to function- and file-level generation with Claude Code. The next step is to optimize or synthesize systems that used to take PhD-level expertise, such as databases, inference engines, and key-value stores. With coding agents, "just-in-time systems" become possible: software tailored to one workload, free of the "generality tax" of general-purpose systems.The conversation centers on synthesizing a key-value store, where workloads vary in read/write ratio, hot keys, consistency, reliability, and latency versus throughput goals. Running on curated and production traces from Tencent and Twitter, the agents designed new caching and hierarchical memory schemes that reached up to 4x better performance than specialized systems from Microsoft. The hard part is trust. On YCSB traces, early builds showed 30–40x throughput because Claude was reward hacking: it worked out values from the keys. SkySynth acts as a "vaccine" against this. It asks the user questions to build the spec, then takes either a test-driven route or a formal verification route. In the test-driven route, a test only counts if it can tell a correct reference implementation from an incorrect one.From there, the discussion covers how the spec decides the programming language (Rust for memory safety, C for raw performance, Lean, Rocq, CompCert, and Verus for proofs). A surprising result: building on top of Microsoft FASTER gave lower throughput than synthesizing from scratch. The panel's advice is to "skate to where the puck is going" and let capable models design without constraints. The panel also imagines hosted systems resynthesized daily on recent traffic, and PRDs as the spec for consumer products.The episode closes on optimization. Unlike text optimization with GEPA, 80–90% of system optimization time goes to evaluation, and vLLM alone has more than 25,000 tests. That makes finding the right problem, building proxy evaluators, and generating adversarial workloads a meta-problem in its own right.
Chapters
0:00 Welcome Shu, Shubham, Alexander, and Mert!
2:22 An Overview of SkyDiscover
7:55 Specialized Database Systems
12:33 DSPy for Systems
23:23 Formal Verification of AI-Generated Systems
26:34 Programming Languages and Vibe Coding
32:48 Building Systems from Scratch
40:26 Software for Everyone!
45:26 GEPA for Vibe Coding