本文提出 NEBULA，一个针对 OAuth 2.0 刷新令牌（refresh token）的、与编程语言无关的精确规格说明，旨在解决 RFC 9700（OAuth 2.0 安全最佳当前实践）中只规定策略而未规定机制的问题。刷新令牌是现代认证系统中极其敏感的凭证：它们长期有效、采用 Bearer 风格，且足以在数天或数周内持续铸造访问令牌。RFC 9700 要求公共客户端签发的刷新令牌必须在每次使用时轮换并具备重放（重用）检测，或采用发送方约束，但该 BCP 并未规定线上格式、存储模式、验证步骤顺序、并发契约，也未定义丢失响应重试或密钥轮换等边界情况的语义。因此，不同实现恰恰会在决定安全结果的关键边界情况上产生分歧。NEBULA 提供了 RFC 9700 刷新令牌模型的精确、语言无关规格，并附带十个符合性参考实现（TypeScript、Python、Go、Rust、Java、PHP、C#、Ruby、Elixir、Dart）。NEBULA 令牌是不透明的——包含 128 位公共选择器和 256 位秘密验证器，两者均由 CSPRNG 输出，不携带声明也不含签名，因此令牌有效性是服务器端状态的属性，而非密码学验证的属性。其一致性方法将行为套件作为数据而非散文发布：38 个场景存储在一个机器可读文件中，每个实现通过一个轻量级语言运行器执行，从而在结构上排除因转录导致的行为漂移。论文描述了该规格，包括一个比较并交换（compare-and-set）的轮换契约，它关闭了并发刷新下重放检测的一个可复现绕过；分析了其安全属性，包括后量子姿态；并报告了跨语言一致性作为多实现安全规格的方法。规格、实现和一致性工件均在 Apache License 2.0 下开源。本文适合身份认证协议设计者、OAuth/OIDC 实现者、安全工程师以及关注安全关键系统形式化与多语言一致性保障的研究人员阅读。