什么值得做
GitHub 开源项目 · 11-6 写
aidenybai/tla-ts · aidenybai

「Java 写的(ew)」:Million.js 作者把 TLA+ 检查器搬进了 npm

它是什么 把 TLA+ 官方那个要装 Java 的模型检查器用 TypeScript 重写了一遍,浏览器和 Node 里都能跑,还能检查证明,结果和官方一致。

为什么火了 9 月 Claude Code 负责人带火了「让 AI 写 TLA+ 做验证」,一批 Web 开发者想试却卡在装 JVM;前端圈大号 Aiden Bai 用「Java 写的(ew)、快两倍、npm 一装」两次发帖,合计约 6 万浏览,star 跟着上了两个台阶。

C你可以怎么跟 别再做 TLA+ 的 TS 版;挑一个老牌但安装劝退的专业工具,让 agent 对着原版测试集移植成 npm 或 WASM 包,README 放一致性结果和基准、配在线 playground,在 X 和 Show HN 用一句「原版难装又慢,现在一键装、更快」发布。

C 级:TLA+ 的 TS 位置已被占住,而且作者 4 万浏览打底也只换来两百多 star,说明这类专业工具的 star 天花板低、很依赖作者自己的流量;能学到一套清楚的选题和发布方法,直接跟进不划算。 小圈子里在传
数据(每天更新) · 建库 2026-10-26 · 237 星 · 7 天 +121
GitHub · 星数
010020010-3011-0111-0311-0611-08237
数据 2026-10-30 → 2026-11-08(10 天,10 次观测)。10-28 以前的点来自 deeply / 存档补录,不是每天都有

2026 年 10 月 28 日,Million.js 和 React Scan 的作者 Aiden Bai 在 X 上发了一条帖子,介绍 tla-ts:一个用 TypeScript 重写的 TLA+ 模型检查器,npm install 就能装,自称比官方的 TLC 快一倍。到 11-06,这个建库才 11 天的仓库 star 刚过两百。量不大,可它是怎么起来的值得拆开看:先有一股「让 AI agent 写 TLA+」的风,再有一个有流量的作者,加上一句前端开发者一听就懂的话。如果你想做一个同样能拿到 star 的开源项目,这里能学的是选题和发布方法,这个位置本身已经有人占了。

一条 4 万浏览的帖子

帖子原文是:「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」。配了一张基准图。到 11-06,这条有 4.01 万浏览、439 赞、243 收藏、42 条回复。

回复里被转得最多的一句来自一个普通用户:「the only way web devs were ever going to touch formal verification was if it came as an npm install」(Web 开发者要碰形式化验证,只能是 npm 一装就能用的那种)。这句话把卖点讲完了。

有个细节:放 GitHub 链接的那条跟帖只有约 2,700 浏览。4 万人看到了帖子,点进仓库的只是一小部分。

它是什么

TLA+ 是一种写「系统该怎么运行」的规格语言,分布式系统、并发协议的人用它在写代码之前找 bug。官方工具 TLC 是 Java 写的,要装 JVM 和 TLA+ Toolbox,很多人卡在安装这一步就放弃了。

tla-ts 做了三件事:

  • 在 JS 里跑。 浏览器、Node、Bun 都行,有一个在线 playground(tla-ts.aidenybai.com),也能在代码里 import { check } from "tla-ts" 当库调。
  • 比 TLC 快。 README 里的基准:单线程下两阶段提交 2.2 倍、哲学家就餐 1.5 倍,542 个一致性模型合计 986 秒对 403 秒。但开 8 个线程、跑 Raft、Paxos 这类大模型,只快 1.1 到 1.5 倍,都是作者自己在 M4 Pro 上测的,没有第三方复现。
  • 结果和 TLC 一致。 那 542 个模型,两边报出来的状态数一个不差。前面几个重写版本都没做到这一步,所以「快两倍」才有人信。

11 月 2 日,它又加上了 TLAPS 证明检查,原本得装一整套 tlapm 才能做的事,现在 npx tla-ts tlapm 一行就行。

star 从哪来

GitHub 每日快照里的 star 曲线,两个台阶正好对着两次发帖:

日期star发生了什么
10-305510-28 发布帖之后
10-31100单日 +45,最多的一天
11-02121发第二条「introducing TLA-ts proofs」,配视频,2.04 万浏览
11-04172两天各涨约 25
11-06191GitHub 实时数是 227(11-06 下午)

作者本人是主渠道。 Aiden Bai 在 GitHub 上有约 5,800 个关注者,名下项目合计 5 万多 star,在 X 的前端圈是大号。两次发帖合计约 6 万浏览。

同圈子的人接了话。 React Compiler 核心成员 lauren(@poteto)10-29 回复「will take a look at supporting tla-ts!」,这条有 1.95 万浏览;她的项目原来用别的 TLA+ 解析器,Aiden 答应去提 PR。这是目前唯一能看到的下游在谈接入,最后接没接上,还看不出来。

时机。 2026-09-22,Claude Code 负责人 Boris Cherny 发帖说用 Opus 5.5 拿 Lean 和 TLA+ 形式化验证 Claude Agent SDK,220 万浏览。之后 reasonable.io 写了《The internet discovers TLA+》,Stack Overflow 博客 10-16 写了「AI says you're right, formal methods say you're wrong」,GitHub 上「让 agent 做形式化验证」的新库明显多了。一批原本不碰 TLA+ 的 Web 开发者想试试,第一道门槛就是 JVM。tla-ts 一个月后把这道门槛拆了(热点和 star 之间的因果是推断)。

没去的地方。 Hacker News、Reddit、Product Hunt 上都找不到发布帖,也没有媒体报道。npm 上日下载从 10-27 的 461 涨到 11-05 的 2.9 万,但它 10 天发了 150 个版本,几乎每次提交都自动发一个包,镜像和扫描器每次都要全量拉一遍,这个数大概率虚高(推断),不能当真实用户数。

它大概率是 agent 写的

仓库里的 AGENTS.md 第一句要求:动手之前先把 tlaplus/tlaplus 克隆到本地,翻 TLC 源码弄清语义,「不要凭记忆或猜测」;行为不清楚就拿 TLC 跑一遍对照。再加上 10 天 150 个版本、两周不到做完模型检查和证明检查,这很像最近一批「让 LLM 对着原版源码和测试集移植大型工具」的做法(推断,作者没明说)。

这一点对想跟的人最重要:以前把一个几十年的 Java 工具重写一遍是一个团队一年的活,现在门槛变成了「有一套能对照的测试 + 一个会指挥 agent 的人」。

谁在抢这个位置

项目形态规模和 tla-ts 的区别
TLC / TLA+ Toolbox官方,Java3,199★标准答案,要 JVM,不能进浏览器
Spectacle(tla-web)浏览器里的 JS 解释器,2021227★最早在浏览器跑 TLA+,官方文档写明比 TLC 慢很多,用来探索和分享规格
tla-checkerRust 重写,2026 年初未核实同样重写 TLC,带 TUI,不是 npm 包,作者没流量
QuintTLA 系的新语法1,926★换了一套语法,tla-ts 保留原版 TLA+
ApalacheScala,SMT 符号检查623★路线不同
Specula、tla-precheck 等让 agent 用 TLA+ 的技能和流水线几十到 629★底下还是调 TLC,tla-ts 可以给它们当引擎

重写 TLC 的人不少,但「npm 包 + 比 TLC 快 + 一致性测试 + 证明检查」凑齐的只有它。在 TS/JS 里再做一个 TLC,目前没看到跟风的,也没必要去做。

如果是你

一句判断: 别再做 TLA+ 的 TS 版,抄它的选题公式:找一个老牌、好用、但安装劝退的专业工具,借 agent 热点,用 agent 对着原版测试集把它移植进 npm 或 WASM。

适合谁: 会指挥 coding agent 做大规模移植、对某个专业领域(形式化验证、图形布局、编译器、科学计算)熟、在 X 或某个开发者社区里有几千关注者的人。

不适合谁: 没有任何发布渠道的人。Aiden Bai 有 4 万浏览打底,也只换来两百多 star。没有流量,同样的东西很可能就停在个位数。

怎么做:

  1. 挑原版:Java、OCaml、Scala 或要装一堆本地依赖,有公开的测试集或示例库能拿来对照(比如 Alloy、PlantUML、各类 SAT/SMT 求解器的前端,哪个合适要你自己判断)。
  2. 让 agent 先读原版源码,每一步都对着原版跑结果;README 里放「N 个模型和原版结果完全一致」加基准表,这是让人信的关键。
  3. 一定要有在线 playground,别人点开就能试。

怎么获客: 在 X 上用一句话发:「X 写的(ew)、不能在浏览器跑、慢 → 现在 npm 一装、快 N 倍」,配基准图;把功能拆成两次发,隔 5 天左右;主动给用得上它的 agent 技能、编辑器插件提 PR 把它接进去;它没去 Hacker News,你可以首发 Show HN。

什么时候之前: 「agent 写形式化验证」这股风是 9 月下旬起来的,用 agent 移植老工具的项目接下来会越来越多,先做的人才能拿到「第一个 npm 版」这个名头。估计窗口在半年以内。

什么情况说明看错了: 如果到 12 月 tla-ts 还在两三百 star、poteto 那边也没接入,说明这类项目的 star 天花板就是作者自己的流量,产品本身拉不动增长;如果官方 TLA+ 出了 WASM 版或浏览器版,这条路在 TLA+ 上就彻底关了。

GitHub 仓库 ↗

研究底稿:竞品表、获客证据、完整研究报告
竞品
名字在哪上线规模它和这家不同在哪
TLC / TLA+ Toolbox（tlaplus/tlaplus）开源1999 年前后（GitHub 2016）3,199★，官方标准Java、要装 JVM、不能在浏览器里跑；tla-ts 对着它的结果做一致性测试，自称快 2 倍
TLAPS / tlapm开源2008 年前后官方证明系统安装很重；tla-ts 在 JS 里检查 TLAPS 证明
Apalache开源2015623★走 SMT 符号检查，Scala 写的，路线不同
Spectacle / tla-web开源2021227★同样是浏览器 JS 解释器，但官方说比 TLC 慢很多、不追求性能；tla-ts 主打快和完整的检查器
Quint开源20211,926★换了一套 TLA 系语法；tla-ts 保留原版 TLA+
tla-checker（Rust）开源2026 年初未核实（Reddit 发布帖）同样是重写 TLC，Rust 写的，带 TUI，没有作者流量，也不是 npm 包
Specula / tla-precheck / proof-skills 等 agent 技能开源2025-06 至 2026-10几十到 629★都是 agent 用 TLA+ 的流水线或技能，底下还是调 TLC；tla-ts 是可以把 JVM 换掉的引擎
用户从哪来
  • 查实 作者 X 发布:10-28 发布帖 40.1K 浏览、439 赞、243 收藏；11-02 发证明检查功能，20.4K 浏览、394 赞；两次发完 star 都跟着上了台阶
  • 查实 同圈子大号互动:React Compiler 核心成员 @poteto 10-29 回复要接入 tla-ts，19.5K 浏览
  • 推断 平台热点（agent 加形式化验证）:Boris Cherny 09-22 发帖说用 Opus 5.5 拿 Lean/TLA+ 验证 Claude Agent SDK，2.2M 浏览；reasonable.io《The internet discovers TLA+》
  • 推断 HN/Reddit/媒体:HN Algolia 和网页搜索都没找到发布帖或报道

aidenybai/tla-ts：为什么能跑出来

渠道：GitHub ｜ 建库 2026-10-26 ｜ 研究日 2026-11-06

一句话

tla-ts 用 TypeScript 重写了 TLA+ 的官方模型检查器 TLC（还能检查 TLAPS 证明），npm install 就能装，浏览器、Node、Bun 里都能跑，作者自己跑的基准里比 TLC 快约 2 倍。它能起来，靠的是三件事叠在一起：作者 Aiden Bai（Million.js 作者，GitHub 约 5,800 关注者，X 上是前端圈的大号）的 X 发布、9 月下旬起「让 AI agent 写 TLA+ 做形式化验证」这股风，还有「Java 写的（ew）→ TypeScript、npm 一装就能用」这个对 Web 开发者很好懂的卖点。从绝对量看它还很小，属于小圈子里在传。

数据

  • star：数据卡（github 库，2026-11-06）191，近 7 天 +136，单日最多 +45（10-31）。曲线：10-30 55 → 10-31 100 → 11-01 116 → 11-02 121 → 11-03 146 → 11-04 172 → 11-05 177 → 11-06 191。GitHub API 现查是 227（2026-11-06 14:29 UTC）。fork 9 个，没上 trending（trending 只收建库约 60 天以上的库，所以这点说明不了什么）。
  • npm：tla-ts 包 10-27 首发，到目前已发 150 个版本（几乎每个 commit 都自动发一个 0.0.3-dev.<sha>），最新 0.0.8，只依赖 fflate。日下载从 10-27 的 461 涨到 11-05 的 29,256（npmjs.org downloads API）。这个下载数明显虚高：版本发得这么密，镜像站和扫描器每次都会全量拉一遍，CI 也会反复装，所以它不代表真实使用量（未核实）。
  • 作者别的库（GitHub API）：cnfast 1,180★、tailwind-stylex 100★ 等；早期的 million、react-scan 是几万 star 级别（数据卡上 owner_total_stars 是 5.33 万）。

竞品（做同一件事的）

产品形态上线规模和 tla-ts 的区别
TLC / TLA+ Toolbox（tlaplus/tlaplus）开源，Java1999 年前后；GitHub 库 2016 年建3,199★官方标准，需要 JVM，不能在浏览器里跑；tla-ts 定位是它的「drop-in 替代」，用 542 个一致性模型对着 TLC 跑结果
TLAPS / tlapm开源，OCaml + 后端证明器2008 年前后官方证明系统安装很重；tla-ts 11-02 起在 JS 里检查 TLAPS 证明
Apalache开源，Scala，符号模型检查2015623★走 SMT 符号检查，路线不同
Spectacle / tla-web（will62794）开源，浏览器里的 JS 解释器2021227★最早的「浏览器里跑 TLA+」；它的官方 wiki 写明比 TLC 慢很多、不追求性能，主要用来探索和分享规格。tla-ts 主打的是速度和完整的检查器
Quint（Informal Systems）开源，TLA 系的新语法20211,926★换了一套语法，自带工具链；tla-ts 保留原版 TLA+
tla-checker（Rust）开源，CLI + Web，带 TUI2026 年初（Reddit r/rust、r/tlaplus 发布帖）规模未核实同样是「重写 TLC」，用的是 Rust，没有作者流量
vscode-tlaplusVS Code 插件2019443★本质是编辑器外壳，底下还是调 TLC
agent 周边：Specula（629★）、kingbootoshi/tla-precheck（112★，TS）、opum-ai/proof-skills、michael-denyer/agent-formal-verify开源2025-06 至 2026-10几十到几百★都是「让 agent 用 TLA+」的技能或流水线，底下还是要 TLC；tla-ts 是它们可以拿来换掉 JVM 的引擎

结论：重写 TLC 这条路上并不缺人（Spectacle 是 JS 版，tla-checker 是 Rust 版），但「npm 包 + 比 TLC 快 + 一致性测试 + 证明检查」这几样凑齐的只有 tla-ts。

增长手段（用户从哪来）

  1. 作者本人在 X 发布，这是主渠道（已确认）。2026-10-28 发的「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」，配一张基准图：40.1K 浏览、439 赞、243 收藏、42 回复（x.com/aidenybai/status/2115477440747413995）。2026-11-02 第二波「introducing TLA-ts proofs」，配视频：20.4K 浏览、394 赞、249 收藏（x.com/aidenybai/status/2117306744523161732）。两波发完，star 都跟着涨了：前者对应 10-30、10-31 的 +45；后者对应 11-03、11-04 各 +25 左右。
  2. 同圈子的人互动（已确认）。React Compiler 核心成员 lauren（@poteto）10-29 回复说「will take a look at supporting tla-ts!」，19.5K 浏览（x.com/poteto/status/2115926914531819595）；Aiden 那边答应给她的项目提 PR，那个项目原来用的是 tla-parser。也就是说，已经有下游项目在考虑接它。
  3. 借了 TLA+ 正火的势（已确认是背景，因果是推断）。2026-09-22 Boris Cherny（Claude Code 负责人）发帖说用 Opus 5.5 拿 Lean + TLA+ 形式化验证 Claude Agent SDK，2.2M 浏览、6.3K 赞（x.com/bcherny/status/2102543349102338309）。reasonable.io 专门写了篇《The internet discovers TLA+》；Stack Overflow 博客 10-16 也写了「AI says you're right, formal methods say you're wrong」。我们的 GitHub 库里，09-20 之后新建的 TLA+、形式化验证 agent 库明显变多（linux-formal、proof-skills、agent-formal-verify、FVjobs 等）。
  4. 零星转述（已确认）。dev-null.sh 上有人转：「no need for using heavy TLC to check TLA+, this one run in the browser」。
  5. 没找到的：HN（Algolia 搜 tla-ts、搜 url 都没有）、Reddit 发布帖、媒体报道、Product Hunt。x-radar 本地语料这次所有查询都返回 0，像是接口那边的问题，所以 X 上二次传播的面没扫全。

为什么跑出来

  • 作者有流量，一条推文就能起步：建库两天后的发布帖拿到 4 万浏览，star 曲线上的两个台阶正好对着两次发帖。
  • 时机好：Boris 9 月那条把「agent 写 TLA+」带火了，一下子多了一批 Web/TS 开发者想试 TLA+，可第一道门槛就是装 JVM 和 Toolbox。tla-ts 一个月后正好把这道门槛拆掉了。
  • 卖点一句话就懂：「Java (ew) → TypeScript」「2× faster」「npm install」，这对 X 上的前端受众很有效（有回复说「the only way web devs were ever going to touch formal verification was if it came as an npm install」，623 浏览）。
  • 能让人信：README 里有和 TLC 对比的基准，542 个一致性模型的状态数和 TLC 完全一致，还有在线 playground。这让「2 倍快」不只是一句口号，前面那几个 JS/Rust 重写都没有做到这一步。
  • 很可能是 agent 写的：AGENTS.md 要求「clone tlaplus/tlaplus，对照 TLC 源码、跑 TLC 对比」，10 天发了 150 个版本，两周不到把模型检查加证明检查都做了。这和最近一批「用 LLM 移植大型工具」的案例是一个思路（比如 tsc-rs）。这条是推断，作者没有明说。

差异化

差异化是三样凑在一起：运行环境（JS 和浏览器）、性能（比 TLC 快）、兼容（一致性套件对着 TLC 验）。前人只占了其中一样：Spectacle 能在浏览器里跑但慢，tla-checker 快但没有分发。它能跑出来，一半靠这个差异化（能被 agent 工具、在线 playground、TS 工具链直接当库嵌进去，poteto 的回应就是证据），另一半靠作者的分发能力。目前 star 主要还是来自作者那两次发帖，产品本身在拉增长的证据还不多（下游接入只有 poteto 这一处在谈）。

可见度与跟风

  • 可见度：小圈子里在传。只有作者自己两条帖子（合计约 6 万浏览）加少量转述，没有媒体、没有 HN，star 也才两百出头。这是开源项目，不存在收入。
  • 跟风：暂时没有。在我们的库里没看到 10-28 之后冒出来的 TS/JS 版 TLC。

能借鉴的

  • 挑一个「老牌、好用、但工具链劝退」的专业工具（JVM、OCaml、本地装一堆东西），借着 agent 热点用 AI 移植成 npm 包或 WASM，在 README 里放上对照原版的一致性测试和基准，在 X 上用一句「X 写的（ew）、更快、一键装」发布。
  • 把功能拆成两次发（先发模型检查，过 5 天再发证明检查），每次都能再吃一波流量。
  • 把它定位成 agent 工具链的底层引擎，主动去找下游项目（比如 poteto 那个）提 PR，把它接进去。

不确定

  • npm 日下载 2.9 万里有多少是真实使用（大概率被 150 个版本的镜像和扫描拉高了）。
  • 「2 倍快」是作者在 M4 Pro 上自己测的，在 8 个 worker 的大模型上只快 1.1 到 1.5 倍；没有第三方复现。
  • 代码是不是主要由 AI 写的：只有 AGENTS.md 和发版节奏这些间接证据。
  • X 上二次传播的规模：x-radar 这次没返回数据，没扫全。
  • poteto 那个项目叫什么、最后有没有接 tla-ts，未核实。

出处

文章由 AI 根据公开数据和我们每天采集的数据写成,数字带出处,推断已标明