Metadata

Preamble. This post came slowly, simmering over months really. So there is some stream of consciousness in here, and a lot of deliberating in public. The post is me learning modular verification and talking myself into it at the same time. Even pep-talking myself, because this is genuinely hard, and the field's standard advice is to avoid modular verification. But the advice is due for revision: LLMs plus TLAPS are quietly changing the economics that made monolithic spec the rational default. The compositionality problem TLA+ is compositional in the abstract sense... In the astral plane, a program execution is an infinite sequence of states, each state giving a value to every variable in an imagined universal state space. A spec is a predicate (yes/no test) on executions, which denotes a set of allowed executions. In this setup, the steps that change variables in other specs look like stuttering to yours. And that enables us to denote composition as a beautiful purely logical conj...

I am a distributed systems researcher. I mostly read and write about distributed systems and lightweight formal methods. But as my blog definition says, the blog is about "distributed systems broadly defined and other curiosities".  The last two years, LLMs were unavoidably the biggest part of those curiosities. However, I was still surprised how much I had written about them, when I went looking for a line I remembered coining. Something like, "LLMs are good at mediocrity, but really fast". I couldn't find the line, but instead I found a pile of my takes on LLMs scattered across the blog, and I figured it was worth collecting them into an index. So here it is, enjoy! I also threw in my overall take on LLMs that has stayed constant through their four years of reign so far.   Hot takes on LLMs Our Collective Bike Shed Moment (June 26) Are We Becoming Architects or Butlers to LLMs? (Feb 26) How LLMs may affect academic writing (Feb 26)  Agentic AI and The Mythi...

Specula is an agentic system that automates the process of software bug finding through authoring and model-checking a spec for the code. It derives TLA+ specifications automatically from the code, checks code-spec conformance through trace validation, model checks the spec to find concurrency bugs, and reproduces the bug at the code layer by writing integration tests with precise timing. I remember reading the Daikon paper "Quickly detecting relevant program invariants" in 2000 and getting impressed by it, and here we are after 26 years, solving the end-to-end problem much better than I ever thought would be possible in a push-button manner in the year of our lord 2026. But somehow, I am still somewhat unsatisfied with the paper. This may be me being hypercritical and trying to get more out of the paper by arguing with it . So bear with me until I resolve (or learn to accept) these problems over time. I know many of the authors of the Specula work, and respect them, and I...

This week, I presented this paper at ICCCN'26. This is joint work with Aleksey Charapko (University of New Hampshire) and my MongoDB colleagues Matt Broadstone, Daniel Gomez Ferro, and Akshat Vig. The paper investigates how to build a metastability tolerant execution control system (ECS) for a database. Why? Modern databases are complex networked systems serving mixed workloads: short queries (that want an answer in milliseconds) sitting next to analytics jobs (that want the CPU for multiple seconds). The arrival rate of requests is effectively unbounded, but of course, the server's resources are not. And, unfortunately, elastic scaling does not save you here. Scaling takes minutes, whereas, overload takes seconds. Admission control tries to guard the front door (more on this later), but the component that mediates contention once requests reach the backend is the execution control system (ECS). Unlike a closed system OS scheduler, which strives for fairness and completeness b...

The Aurora DSQL paper finally dropped . Reading it yesterday was an interesting experience, because I spent two years (2022-23) working with the AWS team that designed and built Aurora DSQL. Since I have been very familiar with the architecture, the paper's overview description of the system didn't excite me much. And if I am being honest, reading the paper also felt a bit dry, most likely because I am not doing the usual extra thinking to explore/understand the ideas in the paper. But taking a step back today, and leaving my subjective experience aside, I will try to elaborate on how the DSQL architecture is actually built on a set of aggressive and opinionated engineering bets.  If I had to explain this architecture in a single sentence (just as I used to do for other teams at AWS) it would be this: We took a traditional monolithic database and blew out every single component into an independent, horizontally scalable service. Exploding the Monolith DSQL divides the database ...

Metastability has been studied in previous work as a self-sustaining degradation in goodput that persists even after the trigger is gone. The degraded state loiters on entirely due to the system's own internal feedback loops (retries, queues), and there is no simple reset button to press in distributed systems. So this is not a rare exotic problem. Since production systems would have already been hardened to handle the obvious failures, what remains is these hard-to-detect emergent failures. The "Metastable Failures in the Wild" paper (OSDI'22) reports 22 incidents across 11 organizations. Four of the 15 major AWS outages in a decade were metastable failures, with durations ranging from 1.5 to 73 hours.  This paper (June 2026) argues that the systems community has treated metastability phenomenologically, which led people to chase symptoms rather than causes. The paper sets out to give the first analytical causal account of these failures. This framing leads to two...

Moving is not for the faint of heart! The surgeon general should issue a warning against moving houses after age 50 . Coordinating our cross-country move was one of the hardest thing I had done. Selling our house in Buffalo, finding a suitable rental house in the Bay Area, figuring out the logistics of the move, getting rid of the furniture we wouldn't transport, boxing everything up, and then on the other side unboxing everything and buying new furniture... It was simply exhausting. Our move has been a long time in the works. For the last 6 years I have been working remotely, first for AWS and then for MongoDB Research, and I have been telling people I would move out of Buffalo any day now. Indeed we could have moved earlier, but we kept putting it off. We waited until my son finished high school, then tried to move last summer. But we got the house on the market too late and it fell through. By then I had already told people I was moving, including an entire table at OSDI 2025. S...

Looking at my peak male physique, and my Keanu Reeves baby face, you would never suspect it, but I recently turned 50. As is the tradition, I thought about writing a post titled "50 Lessons at 50". Unfortunately, I don't have that kind of wisdom. The thing is, I still feel like I'm 18, same age as my son. Turns out this is the secret old guys have been hiding from us all along. You get older only on the outside, but inside you still see yourself as the same young lad. Still, fifty years should count for something. So what did I actually learn? How am I mentally different than my 18-year-old self. Here is my attempt to tally it up.  1. Caution is warranted I finally understand my parents. As you age, you accumulate battle scars, and the scars turn into habits. Anything that can go wrong will go wrong. You forget the cooktop on once, and suddenly you check it three times before leaving the house. True story. You stop diving head-first into a pile of leaves, because ther...