# TLA+ 74 Hacker News commenters recommended TLA+ and 19 criticized it, November 2025 to November 2026. It was recommended in 12 of 13 months; owners who said how long report a median of 0.6 years (5 owners). It meets the Hacker Approved badge rule. **Verdict:** Lets people precisely model concurrent and distributed systems and catch design bugs before coding. Common caveat: harsh syntax and models that drift from the real code. ## Why people recommend it - Precise models of distributed systems (5 comments): "TLA+ (minus the temporal operators) would be still extremely useful for specifying the behavior of concurrent and distributed systems" ([source](https://news.ycombinator.com/item?id=46299957)) "the advantage of something like TLA+ is that the specs can generally be more abstract and as such the checks can be more exhaustive" ([source](https://news.ycombinator.com/item?id=49110450)) "TLA+ is a great way to model certain systems mathematically, because precision in meaning is a great quality" ([source](https://news.ycombinator.com/item?id=46258030)) - Catches bugs before code ships (5 comments): "Running TLA+ via coding agents became a productivity hack for me to quickly catch invariant breaks" ([source](https://news.ycombinator.com/item?id=47680825)) "I was able to find and prevent a catastrophic bug by pointing Opus armed with TLA+ at the problem." ([source](https://news.ycombinator.com/item?id=49866681)) "adding formal verification surfaced 33 classes of bugs, some of which had several instances." ([source](https://news.ycombinator.com/item?id=49869157)) - Clearer thinking about systems (5 comments): "TLA+ gave me new prespective towards debugging, and started treating system crashes as a state problems rather than just code errors." ([source](https://news.ycombinator.com/item?id=46311135)) "If you're after a language that's OSS, has terse notation, and rewires your brain by helping you think more clearly" ([source](https://news.ycombinator.com/item?id=48257679)) "TLA+ is much closer to what I'd recommend if what you want is clearer thinking about programs, systems and state." ([source](https://news.ycombinator.com/item?id=48260584)) - Helps LLM agents write correct code (5 comments): "LLM agents have none of the attentional and motivational constraints of humans so there's no reason not to do things the right way." ([source](https://news.ycombinator.com/item?id=46677784)) "I view a complete TLA+ specification as a kind of metalanguage that can be used with LLMs to generate code from." ([source](https://news.ycombinator.com/item?id=48195688)) "the act of writing a TLA+ model helps the frontier LLMs to write correct executable code" ([source](https://news.ycombinator.com/item?id=49324224)) ## What people warn about - Harsh learning curve and syntax (3 comments): "the accessibility of TLA+, if you come from traditional programming languages, is quite harsh" ([source](https://news.ycombinator.com/item?id=46301673)) "It has super weird syntax, and a whole separate DSL (PlusCal) to give it workable syntax for programs." ([source](https://news.ycombinator.com/item?id=49914375)) "It sounds like the syntax just sucks and there's no way to get around it." ([source](https://news.ycombinator.com/item?id=48199480)) - Spec drifts from actual code (4 comments): "in most cases there is no validation if the TLA+ model actually maps to the e.g. C code that was written" ([source](https://news.ycombinator.com/item?id=46525605)) "It is a headache to write TLA+ and keep the independent spec up2date with the productive code." ([source](https://news.ycombinator.com/item?id=46061008)) "Problem with TLA+ is that it is a completely unrelated tool to the actual programming" ([source](https://news.ycombinator.com/item?id=45797966)) - Weak at atomics and some properties (2 comments): "another thing TLA+ isn't great at is modeling atomics and in particular weak-memory semantics" ([source](https://news.ycombinator.com/item?id=49912416)) "Not really, some components like components have a lot of properties that’s very difficult to modelize." ([source](https://news.ycombinator.com/item?id=46303690)) ## Alternatives hackers recommend - [Quint](https://hackerapproved.com/p/quint.md): 10 recommend ## Cite as Hacker Approved, "TLA+", https://hackerapproved.com/p/tla-plus/ (counts from 1,795,640 Hacker News comments, November 2025 to November 2026).