Metadata

When talking about TLA+, I keep referring to "abstraction" as the most important thing to learn . And it is about the hardest to learn as well. But a contradiction has been bugging me. Aren't CS people already supposed to be good at abstraction? Isn't abstraction supposed to be at the root of OS, networking, software engineering? Abstract Data Types (ADTs) are a staple of every in CS curriculum. So why do I (and every other formal methods/modeling person) see such a large skill gap in abstraction, and flag it as the core, make-or-break skill for modeling? I think I finally get to the root of this cognitive disonance. There are two kinds of "abstraction" conflated under the same umbrella term. Modularity abstraction: This is the traditional abstraction taught in CS curricula as ADTs, APIs, layered design, etc. It is all about encapsulation, drawing boundaries, and hiding internals. Modeling abstraction: This is what I talk about when I talk about abstracti...

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 is a short chapter covering the nuts and bolts of memory allocation in C: malloc(), free(), and the many ways programmers get them wrong. This is part of our series going through OSTEP book chapters. The OSTEP textbook is freely available at Remzi's website if you like to follow along. Stack vs. Heap C gives you two kinds of memory. Stack memory  is automatic: the compiler allocates it when you enter a function and reclaims it when you return. Heap memory  is manual: you allocate it with malloc()  and free it with free() . Let's remember the layout from Chapter 13. The distinction is simple in principle: use the stack for short-lived local data, use the heap for anything that must outlive the current function call. The heap is where the trouble lives. It forces the programmer to reason about object lifetimes at every allocation site. The compiler won't save you; a C program with memory bugs compiles and runs just fine, until it doesn't. The API malloc(size_t siz...

Paxos consensus protocol, despite its many theoretical virtues, is fundamentally rude. One need only look at the way it behaves to see the problem. A leader seizes power. It dictates values. When two leaders happen to propose simultaneously, they do not pause, tip their hats, and work things out over tea. No,  they duel, each furiously incrementing ballot numbers at the other like barbarians engaging in a perpetual pissing contest (please excuse my language). The follower nodes, meanwhile, are reduced to the role of obedient subjects, promising their allegiance to whichever proposer shouts loudest and most recently. Having spent decades studying this rude behavior (with WPaxos , PigPaxos , and through a great many posts on this very blog ) I became convinced that the field had made a fundamental error. We had been asking "how do we reach agreement?" when the real question we should have been asking, all along, was "would it kill you to ask nicely?" It is therefor...

This paper from METR (Model Evaluation & Threat Research) introduces a new metric for tracking AI progress: the "50%-task-completion time horizon". This denotes the length of software engineering task (measured by how long a skilled human developer takes to complete it) that the AI model can finish with 50% success rate. The researchers evaluated 12 frontier AI models on 170 tasks across three benchmarks: HCAST (97 diverse software tasks ranging from 1 minute to 30 hours), RE-Bench (7 difficult ML research engineering tasks, each 8 hours), and SWAA (66 short software actions taking 1-30 seconds). To calibrate task difficulty, they collected over 800 human baselines from professional developers, totaling 2,529 hours of work. The headline finding is that this time horizon has been doubling every 7 months since 2019. GPT-2 could handle tasks that take humans about 2 seconds. The o3 model reached 110 minutes. Extrapolating this trend, AI reaches a one-month time horizon (167...

Chapter 13 of OSTEP provides a primer on how and why modern operating systems abstract physical hardware. This is part of our series going through OSTEP book chapters.  The OSTEP textbook is freely available at Remzi's website if you like to follow along. Multiprogramming and Time Sharing In the early days of computing, machines didn't provide much of a memory abstraction to users. The operating system was essentially a library of routines sitting at the bottom of physical memory, while a single running process occupied the rest of the available space.  I am not that old, but I got to experience this in 2002 through programming sensor nodes with TinyOS . These "motes" were operating on extremely constrained hardware with just 64KB of memory, so there was no complex virtualization. The entire OS and the application were compiled together as a single process, and all memory was statically preallocated. Ah, the joy of debugging a physically distributed multi-node deplo...

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