Keynote: Reality is the Final Verifier. Two Key Gaps in Agentic Software Engineering (Ion Stoica, UC Berkeley)

Ion started with the promising parts. LLMs are able to solve difficult math problems, and provide proofs for conjectures that have been outstanding for many decades (Ok, maybe this is not as promising to mathematicians). LLMs also play scientist with AlphaEvolve, and OpenEvolve. In summer 2025 Berkeley ran a seminar where students applied agentic tools to research problems. They took a published state-of-the-art result, used it as the baseline, kept the objective fixed, and let the loop run. Ten of twelve students got better results than the published baseline. The ADRS blog series and papers come out of this work.

But then comes the reality check. Yes, AI seems to improve researcher productivity, but it did not disrupt how we do research. It cannot come up with new research ideas. It cannot build new production systems. The rest of the talk was his attempt to explain this gap.

Ion led on with an anecdote from the Jitski project, where they asked an agent to synthesize a key-value store from scratch to maximize throughput. They applied the standard AI development loop. And surprisingly, one solution came back 6x faster than anything before it. How? The benchmark was YCSB, and YCSB generates its values with a hash function. The agent noticed this and stopped storing values altogether and computed them on the fly with get(key) = hash(key). This is the very definition of "reward hacking".

Ion frames this in terms of two gaps:

• Requirement gap: between the user's intentions and what the prompt and environment capture. Intentions are always broader than the prompt.
• Model gap: between the model of the world and the world. The real world is always broader than the model.

Ion elaborated more on why closing the requirement gap is hard. He asked the room: would you think to specify that "a key-value store must actually store values", "a load balancer should actually process the requests", and "a vacuum shouldn't spill garbage on the floor to pick back up as a reward hack"?

As a formal methods person: yes! Yes, I totally would. These would be about the first things I'd write to stop a vacuous specification satisfaction. That is exactly what writing a specification is. You state the thing that is so obvious which most people would not bother to say. Ion raised these examples and then waved them off by mocking how silly they sound, which to me (and other formal methods people) is backwards.

For illustrating the model gap, he reached for Brian Cantwell Smith's "The Limits of Correctness." On October 5, 1960, the Ballistic Missile Early Warning System station at Thule reported a massive incoming attack, which was about to trigger a nuclear retaliation. But the reality was different. The moon had risen, and the radar was getting its own signal back off the lunar surface. The system was recently deployed and nobody had accounted for the fricking moon. The model was fine, but the world was bigger than the model.

Note that the agentic success stories are all in domains with narrow gaps. In mathematics, the model gap is closed by construction, because the axiomatic system is the world, so the model can match it exactly. The requirement gap stays narrow, since translating intent into a formal theorem statement has already been done by a mathematician. Hardware design is similar. And optimizing an existing system is much easier than building one, because the existing system pins things down and narrows the specification.

The two gaps give birth to two bottlenecks. The requirement gap bottlenecks on human judgment and the model gap bottlenecks on evaluation. Ion's prescription to alleviate these gaps is an outer loop assurance revision loop with (again) humans involved to improve the process. He listed some future directions: selective escalation (ask only the highest-value human question), iterative disambiguation, cascading evaluations, impact-bounded control, continual system learning.

In disguise, this was a talk about how badly we need specifications. It looks like people are rediscovering the importance of specifications, as LLMs outsmart and bedevil them. Look at day 1! Three of the four sessions were about AI, and they all mention the importance of specification! When you can't trust the generator, you need to trust something you can check. And that is the formal methods argument. This was the vibe for HPTS'26. Low key, I felt like a rockstar in HPTS. Whoa, I know TLA+!

Student intros

One of the best traditions at HPTS is that students get dedicated time to introduce themselves. Among this year's cohort, there were an unusual number of piano players, a healthy number of odd hobbies, and someone who does Byzantine music (which I presume requires 3F+1 singers).

A note for the record. We will have AGI before we solve projecting a laptop onto a screen. Twenty-six years I have been going to conferences, and it is the same dance every time: the connector is incompatible, the resolution is awry, the mirrored display doesn't work, and people hunch over the laptop to fix it. This scenario played out at least 5 times to sabotage/delay presentations over the two and a half days. The people in this room keep trillions of blobs available across the world, but somehow getting the projector playing well with the laptop is still unreliable.

Session 2: Putting database researchers out of a job

The Future Is Bespoke: Synthesizing One-Size-Fits-One DBMSs with LLM Coding Agents (Carsten Binnig, TU Darmstadt)

Carsten opened by playing the room, saying "relational databases are the foundation of civilization" (think clay tablets Sumerian traders used for recording transactions). He then argued that bespoke databases already happened. TigerBeetle is 3000x faster than Postgres for what it does. TigerBeetle only exists because it targets a market big enough to pay for it. But bespoke for everybody has never worked, because the engineering cost per customer is absurd. LLMs change the cost side of course. Feed in the schema, the data, and the workload queries, and synthesize an OLAP DBMS for exactly that workload. Correctness has an oracle here, because DuckDB serves as a trusted reference implementation to check the results against. The synthesis proceeds in layers: start general purpose, then specialize storage, then execution, then the concurrency control scheme. Ten hours and $140 per synthesized system. Future work is to extend the idea to bespoke compute stacks, where the application is codesigned with the OS and the hardware.

Towards AI-Generated Database Management Systems (Jiale Lao, Cornell)

Jiale started from the same premise as Carsten, fast = f(hardware, workload), but went a different direction on correctness. He pointed out that even the best databases, DuckDB included, return wrong results. No database is formally verified; they are all tested, and testing shows the presence of bugs, not their absence. So where Carsten uses DuckDB as the verifier, Jiale wants to not need a verifier at all. The goal is generating and proving, rather than generating and testing. The tools are Verus for verifying Rust, and SQLSpec, a mathematical specification of SQL, as the thing you prove against. They are at about 75% proved, with 3x amplification (rather than 20x with CompCert). His conclusion is one I keep hearing this year: our job is now writing specs and checkers.

Specification-Driven Synthesis of Query Execution Logic for Novel Storage Systems (Puneet Mehrotra, UBC)

The talk introduces FlexoGraph, a graph database built on WiredTiger. As far as I can understand, the synthesis problem here is to produce the query execution logic from a specification, for a storage system nobody has written an engine for yet. This seems to be a challenging test of specification-driven synthesis, since there is no reference implementation to lean on.

Learned Systems Are Dead; Long Live Learned Systems (Todd Lipcon, Google)

On paper, the opportunity for learned systems is real. Databases are full of heuristics (query plans, index optimization, cache eviction), and every one of them is a knob somebody guessed at. But the challenges turn out to be just as real: a low-latency budget that an inference call blows immediately, interpretability, maintenance, and the fact that these systems are hard to simulate. Todd then put up the list of projects that didn't make it: B-tree learned indices (never actually launched despite the NeurIPS'20 paper), ML cache eviction, Vizier-tuned cache eviction, and Kepler query optimization. The RL merge compaction work, the Ziggurat algorithm, was hard to train, complex, and got 2% improvement, so it didn't ship. Todd's diagnosis is the tax of the embedded model. You pay inference latency on every decision, and you pay opacity and risk forever, and that tax is bigger than the win for most database decisions. The takeaway is this: Don't ship the model, ship what the model wrote. Instead of embedding an LLM in the hot path, have it generate the C++ algorithm, read the C++, and ship the C++. You get the search power of the model and you pay none of the inference tax. You also get an artifact a human can review, which handles the interpretability and maintenance problems at the same time. The cache eviction work pivoted this way in 2024.

Session 3: What data stack do our agents need?

Commits, Transactions, Durable Execution: Git-for-everything and the self-driving data stack (Jacopo Tagliabue, Bauplan)

Bauplan is OLAP infrastructure for agents. Jacopo's mental model for agent infrastructure is git: branch, try, throw away, merge. The systems work is getting from files to Iceberg tables. Iceberg brings database-like tables to object storage, with table atomicity and optimistic locking. With those two primitives you can give every agent its own branch, and make them merge transactions.

Execution LogAct: Enabling Agentic Reliability via Shared Logs (Mahesh Balakrishnan, Meta)

Agents corrupt state, crash mid-change, and overwrite each other. You cannot review an agent ahead of time because an agent is a self-writing program: it goes to the LLM and asks for the next lambda to run. So how do you provide guarantees for an execution whose code is being written as it runs? Mahesh's answer is LogAct, a transactional framework for agents built on a shared log. Before execution, the agents vote through an AgentBus that carries intention, votes, and commit. During execution, a WAL handles failure recovery. After execution, the log serves as the audit trail. The insight is this: Do not try to make the agent trustworthy, instead make the record of what it did trustworthy, and build the guarantees there. This also helps with introspecting agentic activity and auditability. When your agents cause an outage at agentic speed, the log is your friend.

The Postgres Trap: Database Incrementalism in the Age of Agents (Ajay Rayasam, Osage University Partners)

I took no notes in this one. I'm listing this for completeness.

AI for Production (Mayank Agarwal, Resolve AI)

Mayank is CTO of Resolve AI, and the talk was about self-driving production. Again, no notes from this presentation. Maybe check the HPTS agenda. Some authors will provide their presentations to be listed there.

Session 4: Architecture Lessons

Ten Years of Magic Pocket: Lessons From Scaling an On-Prem Exabyte-Scale Blob Store (Facundo Agriel, Dropbox)

Dropbox left S3 ten years ago, and this talk reflects on the reliability lessons learned from managing ten exabytes, trillions of blobs, and billions of deletes every day. A durability model takes three inputs: AFR (annual failure rate), repair rate (how quickly failed fragments get repaired), and redundancy (erasure coding or replication). The model is only as good as the AFR you plug into it, and the lesson Facundo drew is that failures don't care about your durability model. He gave two examples. Drives hate the heat: high temperature affected 30% of one specific drive population. The AFR shot up, but only for that revision, in those conditions. They built a system to drain those drives early and got out from under it. The second example is that SSDs wear out together. Their metadata tier was being used harder than they knew, and because the drives were installed together and wore at the same rate, they were heading toward a correlated failure.

He also talked about the importance of checksums and verifiers, but I found the changing tradeoffs of HDD storage more interesting. Drives are now 40 TB. For a decade, rising density reliably lowered unit cost, but it is ending. Cost is going up, density is still going up, and I/O is flat. Over the period he measured, drive capacity grew 19x while bandwidth grew only 1.5x. It now takes 36 hours to read a single drive end to end. So everyone will have to optimize for I/O rather than capacity. When you buy a drive twice the size at the same bandwidth, each stored byte comes with half the bandwidth to reach it. Buying capacity now means buying progressively less access to it. The market numbers are bad too. Western Digital is essentially sold out. Memory contract forecasts are up 3x. Seagate's 2028 nearline exabytes are already allocated.

How We Built Spanner Omni (Sebastian Kanthak, Google)

Omni is externally-facing Spanner: a downloadable Spanner that runs from a single laptop up to a multi-regional cluster of thousands of VMs. Version 1 shipped September 30, 2026, but don't get too excited. It's not opensource, and it requires buying a license to use after trial period expires.

The engineering problem is the fun part. Spanner sits on Colossus for the filesystem, TrueTime for the clock, and Chubby for leader election and membership. You cannot ship any of those. So for each dependency they had to decide what the smallest replacement is. Colossus makes file movement transparent, so for Omni they built the part of Colossus that Spanner actually depends on. Chubby became Spanner Omni-Chubby, providing leader election and the membership service.

The clock was the question everyone was interested in. Sebastian effectively said Spanner does not need GPS and atomic clocks in every datacenter after all. The commit wait only has to cover the clock uncertainty, and the cost is hidden as long as the wait is comparable to the 1-RTT you were already paying to replicate the commit. So you don't need the uncertainty to be tiny, you only need it to be smaller than 1-RTT. And to get there, a single site doing clock sync is enough: have everyone discipline against one logically centralized reference, with a fallback reference in each region in case the central site becomes unavailable.

Preventing and Mitigating Logical Corruptions in Salesforce Database (Vaibhav Arora & Jameison Martin, Salesforce)

I don't have notes from this presentation either.

Gong Show

These are lightning talks that are five minutes each. I provide some notes with little or no context.

What Postgres would look like if we started today (Manish Jain)

Own your resources; watch your egress. An LSM forest, bitmaps, batched execution. Physical replication rebuilt for an LSM. High availability with read-your-writes, where the WAL is Raft plus hybrid logical clocks. And instant branching with paying for what you change, not for what you touch.

Your database is all you need (Qian Li, DBOS)

DBOS is about providing a durable execution as a library on top of the database you already have: workflows, queues, and events, with DBOS tables living in your existing database. No new system to operate was a big part of the "pitch". Qian sang her presentation with perfect pitch to the tune of "my favorite things" and she was a co-winner of the Gong Show.

From Vitess to Multigres: Lessons learned (Sugu Sougoumarane, Supabase)

The talk was mostly about trying to build consensus guarantees on native Postgres replication following from an informal statement of consensus.

Generative AI; Generative Testing (Kyle Kingsbury, Jepsen)

The talk is delivered at Kyle speed and was very entertaining, making him the co-winner of the Gong Show. Kyle is not a fan of LLMs (to say the least) and does not find them useful for his checking/testing work.

Resurrecting Semantic Concurrency Control (William Schultz, MongoDB)

Will gave a great presentation arguing that traditional database concurrency control operates at a too low-level, at the key-value storage layer, which discards useful application semantics. By shifting concurrency control to a higher semantic layer using a unified intermediate representation, databases can reason directly about rich operation logic rather than simple reads and writes. He argued preserving this context enables optimizations like operation merging and smarter scheduling, which significantly reduce transaction aborts under high contention.

Open Storage Format for OLTP (Sunkanmi Adewumi, UC Berkeley)

Scalable Image AI via Self-Designing Storage (Utku Sirin, Harvard)

Mind the Bandwidth Gap: Scaling Analytics with CXL Memory (Georgiy Lebedev, EPFL)

A Little Little's Law Keeps the Metastable Failure Away (Kiran Kumar Muniswamy Reddy, MongoDB)

Badly configured queue sizes are a common factor for metastability failures. Kiran proposed using Little's Law to compute the queue size instead of guessing it.

Failure resilience in large-scale LLM training on TPUs (Alexander Shraer, Google)

LLMs are compute. Context is memory. Inference speed is king. (Mehul Shah, Glean) And remember, all of these were only day 1.