Metadata

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 bare 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...

Ok, finally getting sometime to put my butt down to write about day 2 of BugBash. Why do so few buildings fall down? Brian Potter, Senior Infrastructure Fellow @ Institute for Progress, Author of Construction Physics  newsletter. Buildings rarely collapse. The rate of major structural failing is  between 1/100K to 1/ 1 million. (This is how I know this is a serious statistic: it is an interval.)  Why don't more buildings fall down? There are some technical reasons to it: buildings are simple stuctures with no (or little) moving parts. Buildings exhibit a limited number of behavior when you load their structure: stress, deflection, vibration, creep, etc. And these behaviors are commensurate to the  proportion of the force you put in. Finally, buildings are designed for 2X-3X of expected load. Let's go deeper into structural elements. We have good theories for how structural elements behave, and individual components are tested extensively and are standardized. A build...

These are my notes from the afternoon sessions of BugBash'26 . We had a 75 minute lunch break. Nice lunch, but there were no vegetarian entries, which made Peter Alvaro hangry. I don't blame him, I would be too.  Informal methods Ben Eggers, Member of Technical Staff @ OpenAI This was a fun and also thought provoking talk. The premise is "Nothing has changed about software development". Really? After the LLMs eating software like a wildfire, and particularly rocking at code generation in the last 3 months?? And this is coming from an OpenAI infrastructure engineer, who was once a  8th highest 7d token user. How come?  The talk has two parts: writing code was where the hard parts surfaced agents move the work, but do not obviate it Ok, now it makes more sense. Both of these are sensible statements. Ben followed with a couple disclaimers, that he is talking about deep narrow systems, and not about broad high surface area systems, because he has experience in the former,...

Continuing with notes from the BugBash talks. Yes, all of this goodness, including Will Wilson's keynote was before lunch the first day. Where all the ladders start Peter Alvaro, Associate Professor of Computer Science @ UC Santa Cruz In this talk, Peter reflects back on his 20 years of distributing systems work. The cover image is Don Quixote (which is Peter)  attacking the windmill (robust distributed systems) with a spear (which is some singular solution often borrowed from databases). The first attack was through the use of arcane algebras . This is a purist approach of getting it right the first time. This was during Peter's PhD at UC Berkeley, where Neil Conway was also a peer and collaborator. In his own admission, this was incited by a naive framing around what makes distributed systems difficult? The target was uncertainty regarding order and timing, which cause distributed consistency problems, and require  coordination. But distributed coordination comes at the ...

I attended the BugBash 2026 these last two days, and had a blast. Here are my notes from the first keynote. I will try to find time to publish my notes from the other talks in the coming days. Keynote: We won, what now? Will Wilson, Co-founder & CEO @ Antithesis The Antithesis team opened with a great animation/teaser clip, then Will took the stage. Here is the summary of his talk.  This is not a software testing conference. This is about building reliable software by any means: testing, observability, formal methods, people/culture, better languages. He shows a meme of the five planeteers invoking Captain Planet using their rings. It is time to acknowledge the elephant in the room.  A new contender emerges: AI!! We are now taking a fundamentally unreliable system (AI) to make the systems we are developing reliable. And it is working somehow?! There is a vibe quality to it. When the cost of software generation goes down drastically, you can do a whole lot of it as per Jev...

This paper presents SysMoBench, a benchmark designed to evaluate generative AI's ability to formally model complex concurrent and distributed systems. Although the paper is published on January 2026, the AI landscape moves so fast that the models evaluated (like Claude-Sonnet-4 and GPT-5) already feel dated, after the release of heavy hitters like Claude 3.5 Opus or OpenAI's Codex.  The paper draws a distinction between algorithms/protocols and system modeling. As the paper (somewhat circularly) defines it, "system models enable verification of system code via comprehensive testing and model checking". The paper says: Modeling these systems requires the AI to deeply understand the system design, reason about safety and liveness under unexpected faults, and abstract system behavior into an executable program. This paper is a great paper to follow up my post yesterday on TLA+ Mental Models . It is instructive to see how the paper corroborates my claims in that post. My ...

In the age of LLMs, syntax is no longer the bottleneck for writing, reading, or learning TLA+. People are even getting value by generating TLA+ models and counterexamples directly from Google Docs descriptions of the algorithms. The accidental complexity of TLA+ (its syntax and tooling) is going away. But the intrinsic complexity remains: knowing where to start a model, what to ignore, and how to choose the right abstractions. This is modeling judgment, and it is the hardest skill to teach. Engineers are trained to think in code, control flow, and local state. TLA+ forces you into a different mode: mathematical, declarative, and global. You specify what must hold, not how to achieve it. Once you get comfortable with this shift, it changes how you think about systems, even away from the keyboard. In a companion post , I described TLA+ as a design accelerator based on lessons from 8 industry projects. Here I want to go deeper and articulate the mental models behind effective TLA+ use. Th...

After 15+ years of using TLA+, I now think of it is a design accelerator. One of the purest intellectual pleasures is finding a way to simplify and cut out complexity. TLA+ is a thinking tool that lets you do that. TLA+ forces us out of implementation-shaped and operational reasoning into mathematical declarative reasoning about system behavior. Its global state-transition model and its deliberate fiction of shared memory make complex distributed behavior manageable. Safety and liveness become clear and compact predicates over global state. This makes TLA+ powerful for design discovery. It supports fast exploration of protocol variants and convergence on sound designs before code exists. TLA+ especially shines for distributed/concurrent complex systems. In such systems, complexity exceeds human intuition very quickly. (I often point out to very simple interleaving/nondeterministic execution puzzles to show how much we suck at reasoning about such systems.) Testing is inadequate for su...