Murat
Shortly after I joined MongoDB research, we ran a TLA+ workshop. It was a two-day ordeal. We had a 1.5 days of instruction on TLA+ and syntax, after which we tried to help people get started with modeling. People liked learning about TLA+ on the first day, but except for a person or two, we didn't...
Murat
Chess is a lot trickier than it looks. It has so many rules: castling, en passant, pawn promotion, pinning, the discovered check, and the deadlock case of stalemate.It is a concurrent system, but with a very specific kind of concurrency: interleaved execution. More specifically, taking turns:...
Murat
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,...
Murat
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...
Murat
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...