TLAPlusPlus: A Faster TLA+ Model Checker in C11

In the past few days, I have been working on a fun project: TLAPlusPlus.

While running TLA+ specs for Small Python, one thing that really blocked me was the time it took to run them. I use a lot of TLA+ specs to model the C implementation, and the expensive run time kills me.

I was never into Java. So I asked Claude Code to build one in C11. Just one C file and one header file. I asked it to produce a language specification first, then test262-style test specs, and then use TLC as the oracle. The outcome is amazing: it’s slightly faster than the official Java version. v0.1.0

Making it actually pass all the Small Python TLA+ specs is a real-world testament. To make that happen, more bugs were fixed. v0.2.0

I wasn’t satisfied. I wanted it faster. So after another overnight session, v0.4.0 made it 4x-20x faster than TLC.

I wanted to share it with the world, but I wasn’t confident it actually worked well. So I asked the agent to find more real-world examples, and in turn it fixed more bugs. v0.5.0

I shared it with the Reddit community (post) and got some good feedback from Markus Alexander Kuppe (core TLA+ maintainer) and Fabrício Bracht (author of TLA-RS). v0.6.1 was made from that feedback while I was playing chess, Chinese chess, poker, and football with my family on Sunday.

So this is the short story of making software that actually solves my own pain and can benefit others.