TLAPlusPlus: A Faster TLA+ Model Checker in C11

Developer soasme released TLAPlusPlus, a TLA+ model checker written in C11 as a single C file and one header file, built with Claude Code and validated against TLC as an oracle. Version 0.4.0 of TLAPlusPlus runs 4x to 20x faster than the official Java-based TLC, according to the developer, after v0.1.0 came in only slightly faster and v0.2.0 passed the Small Python TLA+ specs. Feedback from TLA+ core maintainer Markus Alexander Kuppe and TLA-RS author Fabrício Bracht shaped v0.6.1, the current release.

TLAPlusPlus: A Faster TLA+ Model Checker in C11 In the past few days, I have been working on a fun project: TLAPlusPlus https://github.com/soasme/tlaplusplus . While running TLA+ specs for Small Python https://github.com/soasme/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 https://github.com/soasme/tlaplusplus/releases release-v0.1.0 Making it actually pass all the Small Python TLA+ specs https://github.com/soasme/small-python/tree/main/tests/tla is a real-world testament. To make that happen, more bugs were fixed. v0.2.0 https://github.com/soasme/tlaplusplus/releases release-v0.2.0 I wasn’t satisfied. I wanted it faster. So after another overnight session, v0.4.0 https://github.com/soasme/tlaplusplus/releases release-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 https://github.com/soasme/tlaplusplus/releases release-v0.5.0 I shared it with the Reddit community post https://www.reddit.com/r/tlaplus/s/bqGusinwxy and got some good feedback from Markus Alexander Kuppe core TLA+ maintainer and Fabrício Bracht author of TLA-RS . v0.6.1 https://github.com/soasme/tlaplusplus/releases release-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.