是判定，
不是猜测。

Taumorrow Chess —— 不会虚张声势的国际象棋引擎

这个引擎的每一步都由逻辑判定，而不是由网络估计。让搜索更快的捷径，只有在有判定证明表明它们绝不改变结果时才被采纳。它公开地与前沿语言模型实时对弈，并在思考时展示自己对局面的判断。

它所学的一切都来自自己的对局，并经过在任何改动被接受之前就已判定的闸门。与语言模型的对局是实力的度量，从不是训练材料。

The Round as a Formula —— 每一轮都可复算的多人游戏

彩票、共享奖池、一手牌、棋盘上的一步、与庄家对局：多方同时行动、由一步决定整轮的游戏。通常这一步是运营方运行的程序，你只能信任它。在这里，这一轮是一个公式，每一方都能从记录中重新计算它，而记录无法被改写。

该方法始于 2025 年 12 月的白皮书，现已作为论文发表，附有第三方可以重复的执行过程。

AXIOM —— 一个“公式即实现”的游戏

一款二至四人、同时行动的桌面游戏，于 2025 年 12 月建成，是该方法的一次生产环境演示。由全体玩家的承诺生成的骰子、碰撞、状态转移和胜者，都不是先由程序计算再加以检查：每一项都是一条 Tau 语言公式，公式本身就是实现。周围的服务只负责传递消息。

每一轮结束后，任何人都可以下载规范和记录下来的输入并重新综合。输出要么一致，要么暴露出不一致。“Tau is the engine, everything else delivers messages”这句话由此而来，公平游戏的工作也从这里开始。

A Playable Nomic —— 改规则本身就是游戏的游戏

Nomic 自 1982 年起就有人在玩。在它被计算机化的地方，机器执行玩家编写的规则。在这里，机器还会在规则修改生效之前，判定它相对于宪章是否合法；并且一个被固化的核心已被证明能经受住任何合法步骤序列。

在可判定基底上的两级自我修订：玩家修改规则，规则无法改变已被证明的东西。

Orbit 37 —— 37 格的轮盘

四个座位对阵庄家。每次开出前，每个座位和庄家各封存一个数字；一条 Tau 语言的公式把它们按模 37 相加。封存之后，没有人能更改号码格。庄家只能拒绝揭示，而一旦拒绝，就要以筹码支付所有有效投注，视同中奖，对局随即结束。

每一轮完成的对局都是一条签名记录，页面和任何人都可以复算。筹码是没有价值的游戏币：不能购买、出售、转让或兑现。

为什么先做轮盘：在与庄家对战的游戏里，通常所有牌都在运营方手中。它开出结果，它支付，它记账。这是最难建立信任的情形，所以它是这一方法的第一个案例。在 Orbit 37 中，每个座位和庄家都在开出前封存一个数字，号码格是这些数字按模 37 相加的和，庄家只能拒绝揭示。目标是一个运营方在封存之后无法更改号码格的游戏；轮盘只是演示这一方法最简单的载体。