"Written in Java (ew)": the Million.js author moved the TLA+ checker to npm
What it is A rewrite of TLA+'s official model checker, which requires Java, in TypeScript. It runs in the browser and in Node, and can check proofs, with results matching the official tool.
Why it took off In September, the lead of Claude Code made "having AI write TLA+ for verification" popular. Many web developers wanted to try it but got stuck installing the JVM. Aiden Bai, a big name in the frontend community, posted twice with "written in Java (ew), twice as fast, one npm install," for roughly 60k views combined, and the stars climbed two steps alongside.
CHow you could follow this Don't build another TypeScript version of TLA+. Instead, pick an established but hard-to-install professional tool, have an agent port it against the original's test suite into an npm or WASM package, publish consistency results and benchmarks in the README, add an online playground, and launch on X and Show HN with a line like "The original is hard to install and slow. Now it's one install and faster."
- Data (updated daily) · Repo created 2026-10-26 · 237 stars · 7 days +121
GitHub · stars Data 2026-10-30 → 2026-11-08 (10 days, 10 observations). Points before 10-28 come from deeply / archive backfill, not every day has one
On 2026 Oct 28, Aiden Bai, the author of Million.js and React Scan, posted on X about tla-ts: a TLA+ model checker rewritten in TypeScript that installs with npm install and claims to be twice as fast as the official TLC. By 11-06, the repo, which was only 11 days old, had just passed two hundred stars. The numbers aren't huge, but how it got going is worth breaking down. There was a wave of "have AI agents write TLA+," a creator with an audience, and one line that frontend developers immediately understood. If you want to build an open-source project that earns stars the same way, what you can learn here is the method for choosing a topic and launching, and this particular spot has already been taken.
A post with 40k views
The original post read: "Introducing TLA-ts. A 2× faster drop-in replacement for TLC, written 100% in TypeScript. Why? TLA+ for formal verification and model checking is great!... but is written in Java (ew), unusable in browser, and slow." It included a benchmark chart. By 11-06, the post had 40.1k views, 439 likes, 243 bookmarks, and 42 replies.
The most-quoted reply came from an ordinary user: "the only way web devs were ever going to touch formal verification was if it came as an npm install." That line sums up the selling point.
One detail: the reply with the GitHub link got only about 2,700 views. 40k people saw the post, and only a small fraction clicked through to the repo.
What it is
TLA+ is a specification language for describing how a system should behave. People building distributed systems and concurrent protocols use it to find bugs before writing code. The official tool, TLC, is written in Java and requires the JVM and the TLA+ Toolbox, and many people gave up at the installation step.
tla-ts does three things:
- It runs in JS. It works in the browser, Node, and Bun. There is an online playground (tla-ts.aidenybai.com), and you can use it as a library in code with
import { check } from "tla-ts". - It's faster than TLC. Benchmarks from the README: single-threaded two-phase commit is 2.2× faster and dining philosophers is 1.5× faster, and across 542 consistency models the total went from 403 seconds to 986 seconds. But with 8 threads, or with larger models like Raft and Paxos, the speedup is only 1.1 to 1.5×. All of these were measured by the author on an M4 Pro, with no third-party reproduction.
- Results match TLC. For all 542 models, both tools report the same number of states. Earlier rewrites didn't achieve this, which is why people believed "twice as fast."
Nov 2, it added TLAPS proof checking too. What used to require installing the whole tlapm toolchain now takes one line: npx tla-ts tlapm.
Where the stars came from
The star curve from GitHub's daily snapshots, where the two steps line up with the two posts:
| Date | star | What happened |
|---|---|---|
| 10-30 | 55 | 10-28 After the launch post |
| 10-31 | 100 | Single-day gain of +45, the biggest day |
| 11-02 | 121 | The second post, "introducing TLA-ts proofs," with a video, 20.4k views |
| 11-04 | 172 | Each of the two days added about 25 |
| 11-06 | 191 | Live GitHub count is 227 (11-06 afternoon) |
The author is the main channel. Aiden Bai has about 5,800 followers on GitHub, and his projects add up to over 50k stars. On X he's a big name in front-end circles. His two posts together drew about 60k views.
People in the same circle replied. lauren (@poteto), a core member of React Compiler, wrote "will take a look at supporting tla-ts!" in reply 10-29. It got 19.5k views. Her project used a different TLA+ parser, and Aiden said he'd send a PR. This is the only sign so far of a downstream project talking about adopting it. Whether it actually landed is still unclear.
Timing. On 2026-09-22, Boris Cherny, head of Claude Code, posted that he used Opus 5.5 to run Lean and TLA+ formal verification on the Claude Agent SDK. It got 2.2M views. After that, reasonable.io published "The internet discovers TLA+", a Stack Overflow blog ran "AI says you're right, formal methods say you're wrong" 10-16, and GitHub saw a clear rise in new repos for "agents doing formal verification". A wave of web developers who had never touched TLA+ wanted to try it, and the first barrier was the JVM. Roughly a month later, tla-ts removed that barrier. (The link between the trend and the stars is my inference.)
Where it didn't go. No launch posts on Hacker News, Reddit, or Product Hunt, and no press coverage. On npm, daily downloads went from 10-27 to 461 and then 11-05 to 29k. But it published 150 versions in 10 days, nearly every commit auto-publishes a package, and mirrors and scanners re-pull everything each time. The number is most likely inflated (my inference) and shouldn't be read as real users.
It's most likely written by an agent.
The first line of AGENTS.md in the repo says: before doing anything, clone tlaplus/tlaplus locally, read the TLC source to understand the semantics, and "don't rely on memory or guesswork". When behavior is unclear, run TLC and compare. Add 10 days and 150 versions, with model checking and proof checking done in under two weeks. This looks a lot like the recent approach of having an LLM port a large tool against the original source and test suite (inference; the author didn't say so).
This is the part that matters most for anyone who wants to follow it: rewriting a decades-old Java tool used to be a year's work for a team. Now the bar is "a test suite you can compare against, plus someone who can direct an agent."
Who's competing for this spot
| Project | Form | Scale | How tla-ts differs |
|---|---|---|---|
| TLC / TLA+ Toolbox | Official, Java | 3,199★ | The standard answer. Needs the JVM and can't run in a browser. |
| Spectacle(tla-web) | A JS interpreter that runs in the browser, 2021 | 227★ | The earliest way to run TLA+ in a browser. Official docs say it's much slower than TLC and it's meant for exploring and sharing specs. |
| tla-checker | A Rust rewrite, early 2026 | Not verified | Also rewrites TLC, with a TUI. Not an npm package, and its author has no reach. |
| Quint | A newer TLA-family syntax | 1,926★ | Changes the syntax to a different one. tla-ts keeps the original TLA+. |
| Apalache | Scala, symbolic checking with SMT | 623★ | Different approach |
| Specula, tla-precheck, etc. | Agent skills and pipelines for using TLA+ | A few dozen to 629★ | They still call TLC underneath. tla-ts could serve as the engine they swap in. |
Plenty of people have rewritten TLC, but only tla-ts combines "npm package + faster than TLC + conformance tests + proof checking." I haven't seen anyone copying it to build yet another TLC in TS/JS, and there's no real reason to.
If it were you
One-line take: don't build another TS version of TLA+. Copy the topic formula: pick an old, well-regarded, hard-to-install specialist tool, ride the agent trend, and use an agent to port it into npm or WASM against the original's test suite.
Who it suits: people who can direct a coding agent through a large port, who know a specialist domain well (formal verification, graph layout, compilers, scientific computing), and who have a few thousand followers on X or in a developer community.
Who it doesn't suit: anyone without a distribution channel. Aiden Bai had 40k views to start with and still only got a couple hundred stars. Without reach, the same project can easily stall at single digits.
How to do it:
- Pick originals that are Java, OCaml, or Scala, or that need a pile of local dependencies, and that have a public test suite or example library to check against (e.g., Alloy, PlantUML, front ends for various SAT/SMT solvers; which fits is up to you to judge).
- Have the agent read the original source first and check every step against the original's output. The README should state "N models match the original exactly" with a benchmark table. That's what makes people believe it.
- Always ship an online playground so people can try it with one click.
How to get users: on X, post a one-liner like "written in X (ew), won't run in the browser, slow → now one npm install, N× faster," with a benchmark chart. Split the features into two posts about 5 days apart. Send PRs to agent skills and editor plugins that could use it. It didn't go to Hacker News, so you could launch with a Show HN.
How early you need to be: the "agents doing formal verification" wave started in late September. More projects that port old tools with agents will follow, so whoever goes first gets the "first npm version" label. Estimated window: under six months.
What would mean you read it wrong: if tla-ts is still at a couple hundred to three hundred stars by December and poteto's project hasn't adopted it, the star ceiling for this kind of project is set by the author's own reach, and the product alone can't drive growth. If the official TLA+ project ships a WASM or browser version, this path is closed for TLA+.
Research notes: competitor table, acquisition evidence, full research report
- Competitors
Name Where Launched Scale How it differs from this one TLC / TLA+ Toolbox (tlaplus/tlaplus) Open source Around 1999 (GitHub 2016) 3,199★, the official standard Java, needs a JVM, can't run in the browser. tla-ts checks its results against this one with conformance tests and claims to be 2× faster. TLAPS / tlapm Open source Around 2008 Official proof system Heavy to install. tla-ts checks TLAPS proofs in JS. Apalache Open source 2015 623★ Uses SMT symbolic checking, written in Scala. Different approach. Spectacle / tla-web Open source 2021 227★ Also a JS interpreter for the browser, but the official docs say it's much slower than TLC and doesn't aim for performance. tla-ts focuses on speed and a complete checker. Quint Open source 2021 1,926★ Uses a different TLA-family syntax. tla-ts keeps the original TLA+. tla-checker (Rust) Open source Early 2026 Unverified (Reddit launch post) Also rewrites TLC, in Rust, with a TUI. No author reach, and it's not an npm package. Specula / tla-precheck / proof-skills and other agent skills Open source 2025-06 to 2026-10 A few dozen to 629★ All are agent pipelines or skills for using TLA+, and they still call TLC underneath. tla-ts is an engine that could replace the JVM. - Where users come from
- Verified from the author's X posts: the launch tweet got 10-28 40.1K views, 439 likes and 243 bookmarks; 11-02 posted about the proof-checking feature, 20.4K views and 394 likes. Each of the two posts was followed by a step up in stars.
- Verified big accounts in the same circle engaging: React Compiler core member @poteto 10-29 replied wanting to integrate tla-ts, 19.5K views
- Inferred Platform trend (agents plus formal verification): Boris Cherny posted on 09-22 that he used Opus 5.5 to verify the Claude Agent SDK with Lean/TLA+. It drew 2.2M views. reasonable.io published "The internet discovers TLA+".
- Inferred HN / Reddit / press: HN Algolia and web search turned up no launch posts or coverage.
aidenybai/tla-ts: why it runs
Channel: GitHub | repo created 2026-10-26 | research day 2026-11-06
One line
tla-ts rewrites TLA+'s official model checker TLC in TypeScript (and also checks TLAPS proofs). Install it with npm install, and it runs in the browser, Node, and Bun. In the author's own benchmarks it's about 2× faster than TLC. It took off because of three things combined: author Aiden Bai's X launch (he made Million.js and has about 5,800 GitHub followers, and he's a big name in front-end circles on X), the wave since late September of "AI agents writing TLA+ for formal verification," and a pitch web developers instantly get: it was written in Java (ew), now it's TypeScript, and one npm install is all it takes. In absolute numbers it's still small. It's circulating within a niche.
Data
- Stars: data card (GitHub repo, 2026-11-06) 191, +136 over the last 7 days, peak single day +45 (10-31). Curve: 10-30 55 → 10-31 100 → 11-01 116 → 11-02 121 → 11-03 146 → 11-04 172 → 11-05 177 → 11-06 191. Live GitHub API reading: 227 (2026-11-06 14:29 UTC). 9 forks. Not on trending (trending only lists repos older than about 60 days, so that tells us nothing).
- npm: the
tla-tspackage first published on 10-27. It has 150 versions so far (nearly every commit auto-publishes a0.0.3-dev.<sha>). Latest is 0.0.8, and its only dependency is fflate. Daily downloads went from 10-27 to 11-05 29,256 from 461 (npmjs.org downloads API). This download count is clearly inflated: with versions published this often, mirrors and scanners re-pull everything each time, and CI reinstalls repeatedly, so it doesn't represent real usage (unverified). - The author's other repos (GitHub API): cnfast 1,180★, tailwind-stylex 100★, and so on. His earlier projects, million and react-scan, are in the tens of thousands of stars (the data card shows owner_total_stars at 53.3k).
Competitors (doing the same thing)
| Product | Form | Launched | Scale | How tla-ts differs |
|---|---|---|---|---|
| TLC / TLA+ Toolbox (tlaplus/tlaplus) | Open source, Java | Around 1999; GitHub repo created 2016 | 3,199★ | The official standard. Needs the JVM and can't run in the browser. tla-ts positions itself as its "drop-in replacement" and checks results against TLC using 542 conformance models. |
| TLAPS / tlapm | Open source, OCaml + backend prover | Around 2008 | Official proof system | Heavy to install; tla-ts 11-02 checks TLAPS proofs in JS |
| Apalache | Open source, Scala, symbolic model checking | 2015 | 623★ | Goes through SMT symbolic checking, a different route |
| Spectacle / tla-web (will62794) | Open source, JS interpreter that runs in the browser | 2021 | 227★ | The earliest "TLA+ in the browser"; its official wiki says it is much slower than TLC and doesn't aim for performance, mainly used for exploring and sharing specs. tla-ts focuses on speed and a complete checker |
| Quint (Informal Systems) | Open source, a new syntax in the TLA family | 2021 | 1,926★ | Changes the syntax and ships its own toolchain; tla-ts keeps the original TLA+ |
| tla-checker (Rust) | Open source, CLI + Web, with a TUI | Early 2026 (Reddit r/rust, r/tlaplus launch posts) | Scale unverified | Also a "rewrite of TLC", in Rust, with no author traffic |
| vscode-tlaplus | VS Code extension | 2019 | 443★ | Essentially an editor shell that still calls TLC underneath |
| Agent-adjacent projects: Specula (629★), kingbootoshi/tla-precheck (112★, TS), opum-ai/proof-skills, michael-denyer/agent-formal-verify | Open source | 2025-06 to 2026-10 | Tens to hundreds of ★ | All are skills or pipelines that let agents use TLA+, still relying on TLC underneath; tla-ts is the engine they could swap the JVM out for |
Bottom line: the road of rewriting TLC isn't empty (Spectacle is a JS version, tla-checker a Rust one), but tla-ts is the only one that combines npm packaging, speed over TLC, conformance testing, and proof checking.
Growth tactics (where users come from)
- Posted by the author on X. This is the main channel (confirmed). 2026-10-28 posted "Introducing TLA-ts: A 2× faster drop-in replacement for TLC, written 100% in TypeScript… TLC is written in Java (ew), unusable in browser, and slow", with a benchmark chart: 40.1K views, 439 likes, 243 bookmarks, 42 replies (x.com/aidenybai/status/2115477440747413995). 2026-11-02 second wave, "introducing TLA-ts proofs", with a video: 20.4K views, 394 likes, 249 bookmarks (x.com/aidenybai/status/2117306744523161732). After both waves, stars climbed too: the first matches 10-30 and 10-31 of +45; the second matches 11-03 and 11-04, each up roughly +25.
- Direct engagement from people in the same circle (confirmed). React Compiler core member lauren (@poteto) replied 10-29 "will take a look at supporting tla-ts!", with 19.5K views (x.com/poteto/status/2115926914531819595). Aiden also agreed to open a PR for her project, which was previously using tla-parser. In other words, a downstream project is already considering adopting it.
- Rode the wave of TLA+ being hot (confirmed as background, causality is inferred). 2026-09-22 Boris Cherny (head of Claude Code) posted about using Opus 5.5 to formally verify the Claude Agent SDK with Lean + TLA+, 2.2M views and 6.3K likes (x.com/bcherny/status/2102543349102338309). reasonable.io published a piece titled "The internet discovers TLA+"; a Stack Overflow blog post 10-16 also ran "AI says you're right, formal methods say you're wrong". In our GitHub library, new TLA+ and formal-verification agent repos created after 09-20 clearly increased (linux-formal, proof-skills, agent-formal-verify, FVjobs, etc.).
- Sporadic reposts (confirmed). On dev-null.sh someone shared: "no need for using heavy TLC to check TLA+, this one runs in the browser".
- Not found: HN (Algolia searches for tla-ts and the URL return nothing), Reddit launch posts, media coverage, Product Hunt. The local x-radar corpus returned 0 for every query this time, which looks like an interface problem, so the secondary spread on X hasn't been fully scanned.
Why it took off
- The author has reach; one tweet is enough to get started: the launch post two days after the repo was created got 40K views, and the two steps on the star curve line up with the two posts.
- Good timing: Boris's September post popularized "agents writing TLA+", suddenly adding a batch of Web/TS developers who wanted to try TLA+, but the first barrier was installing the JVM and Toolbox. A month later tla-ts removed that barrier.
- The pitch is understood in one line: "Java (ew) → TypeScript", "2× faster", "npm install". This works well with the frontend audience on X (one reply said "the only way web devs were ever going to touch formal verification was if it came as an npm install", 623 views).
- Makes it believable: the README has benchmarks against TLC, state counts for 542 consistency models match TLC exactly, and there's an online playground. This turns "2× faster" from a slogan into something checkable, which the earlier JS/Rust rewrites never did.
- Likely written by an agent: AGENTS.md requires "clone tlaplus/tlaplus, compare against the TLC source, run TLC side by side"; 10 days produced 150 versions, and in under two weeks both model checking and proof checking were done. This follows the same approach as the recent batch of cases using LLMs to port large tools (e.g. tsc-rs). This is an inference; the author hasn't stated it.
Differentiation
The differentiation is three things combined: runtime (JS and the browser), performance (faster than TLC), and compatibility (conformance suite checked against TLC). Predecessors each took only one: Spectacle runs in the browser but is slow, tla-checker is fast but wasn't distributed. It can get traction partly because of this differentiation (it can be embedded directly as a library in agent tooling, an online playground, and TS toolchains; poteto's reply is the evidence), and partly because of the author's distribution ability. So far the stars mostly come from the author's two posts, and there's little evidence the product itself is driving growth (only poteto's downstream adoption is under discussion).
Visibility and copycats
- Visibility: circulating in small circles. Only the author's own two posts (about 60K views combined) plus a few reposts, no media, no HN, and just over two hundred stars. It's an open-source project, so there is no revenue.
- Copycats: none for now. In our library, no TS/JS version of TLC has appeared since 10-28.
What to borrow
- Pick a professional tool that is "old, good, but has a barrier from its toolchain" (JVM, OCaml, lots to install locally), use AI to port it into an npm package or WASM while riding the agent trend, put conformance tests and benchmarks against the original in the README, and launch on X with a one-liner like "X written in Y (ew), faster, one-command install".
- Split features into two launches (model checking first, proof checking 5 days later), so each one can catch another wave of traffic.
- Position it as the underlying engine of the agent toolchain, proactively reach out to downstream projects (like poteto's) and open PRs to integrate it.
Uncertain
- How much of the npm daily downloads of 29K is real usage (likely inflated by mirrors and scanners across 150 versions).
- "2× faster" was measured by the author himself on an M4 Pro; on larger models with 8 workers it is only 1.1 to 1.5× faster. No third-party reproduction.
- Whether the code was mainly written by AI: only indirect evidence such as AGENTS.md and the release cadence.
- Scale of the secondary spread on X: x-radar returned no data this time, so it wasn't fully scanned.
- What poteto's project is called and whether it ultimately adopted tla-ts: not verified.
Sources
- github.com/aidenybai/tla-ts (README, AGENTS.md)
- tla-ts.aidenybai.com/
- registry.npmjs.org/tla-ts, api.npmjs.org/downloads/range/last-month/tla-ts
- x.com/aidenybai/status/2115477440747413995, x.com/aidenybai/status/2117306744523161732, x.com/poteto/status/2115926914531819595, x.com/bcherny/status/2102543349102338309
- reasonable.io/blog/tla-tutorial/, stackoverflow.blog/2026/10/16/formal-methods-say-you-re-wron…, docs.tlapl.us/using:tla_web_explorer, dev-null.sh/@Hasnayeen/commits/01a19de0-a8d6-71b5-ba53-fdc85…
- GitHub API (star counts for tlaplus/tlaplus, apalache-mc/apalache, will62794/spectacle, quint-co/quint, tlaplus/vscode-tlaplus), 2026-11-06; our github library repo_profile (2026-11-06)