Manyan: A Faster TLA+ Model Checker in C11

In the past few days, I have been working on a fun project: Manyan, formerly 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.

Kuppe also suggested tlaplus/examples to me, and I gave it another bench. That is nice: a 20x speed-up, with 70% of the examples covered (the rest are Java-specific or use Apalache symbols).

Kuppe also suggested a rename. I took it seriously and renamed it Manyan. Manyan (曼衍, màn yǎn, said “mahn-yen”) comes from Zhuangzi’s Qi Wu Lun (齐物论): “和之以天倪，因之以曼衍.” It evokes continuous unfolding and transformation.

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