LemmaScript：通过 Dafny 验证 TypeScript 的工具链
摘要
LemmaScript 是一套全新工具链，可将 TypeScript 编译为 Dafny 进行形式化验证，无需改动运行时，并已通过验证 Hono 框架中一个 CVE 修复实例加以演示。
<p><a href="https://lobste.rs/s/4tuujf/lemmascript_verification_toolchain_for">评论</a></p>
查看缓存全文
缓存时间: 2026/04/22 17:24
# LemmaScript：通过 Dafny 验证 TypeScript 的工具链
来源：https://midspiral.com/blog/lemmascript-a-verification-toolchain-for-typescript/
在验证代码时，我们应尽可能让被验证的模型与最终执行的代码保持紧密对应。我们已在 Web 应用场景中探索了一种实现方式：借助 [dafny-replay](https://github.com/metareflection/dafny-replay) 和 [lemmafit](https://github.com/midspiral/lemmafit)，先用支持验证的 Dafny 语言编写业务逻辑，再将其编译为 JavaScript，最后让 React 前端直接调用编译后的逻辑。
该方案在“绿地”项目中表现良好，但也暴露出一些问题，促使我们寻找新思路：
- Dafny 编译步骤会在“Dafny-编译出的 JS”与系统其余部分之间引入集成摩擦
- 难以应用于“棕地”场景——代码早已存在于既有生态（如 TypeScript）之中
为此，我们打造了 [LemmaScript](https://github.com/midspiral/LemmaScript)：把 TypeScript 源码编译成 Dafny（或 Lean），仅用于生成可验证的模型，而可执行链路保持不变，验证链路则作为补充，用来证明正确性。
类似思路已有先例：Rust 的 [Verus](https://github.com/verus-lang/verus)、C 的 [Frama-C](https://github.com/Frama-C) 均属此类。
## 示例：在 Hono 中就地验证 `trimCookieWhitespace` 的棕地场景
下面给出 Hono Web 框架的一个工具函数。受 CVE-2026-39410 启发，我们用 LemmaScript 就地证明：该函数仅剔除空格（0x20）和制表符（0x09），而不会误伤其他字符（如 0xA0）。
做法是在代码中插入 `// @ verify`、`// @ ensures`、`// @ invariant` 等纯注释；对 TypeScript 而言它们毫无副作用，但 LemmaScript 会将其提取并生成验证脚手架。
凭借下列注解，Dafny 可证明所有 `@ ensures` 对任意输入/输出恒成立，从而确认 CVE 修复正确。
```ts
const trimCookieWhitespace = (value: string): string => {
//@ verify
//@ ensures \result.length <= value.length
// CVE-2026-39410: only space (0x20) and tab (0x09) are stripped — nothing else (e.g. 0xA0) is removed.
//@ ensures exists(start: int, exists(end: int, start >= 0 && start <= end && end <= value.length && \result === value.slice(start, end) && forall(i: int, i >= 0 && i < start ==> value.charCodeAt(i) === 0x20 || value.charCodeAt(i) === 0x09) && forall(i: int, i >= end && i < value.length ==> value.charCodeAt(i) === 0x20 || value.charCodeAt(i) === 0x09)))
//@ ensures \result.length > 0 ==> \result.charCodeAt(0) !== 0x20 && \result.charCodeAt(0) !== 0x09
//@ ensures \result.length > 0 ==> \result.charCodeAt(\result.length - 1) !== 0x20 && \result.charCodeAt(\result.length - 1) !== 0x09
let start = 0
let end = value.length
while (start < end) {
//@ invariant start >= 0 && start <= end && end <= value.length
//@ invariant forall(i: int, i >= 0 && i < start ==> value.charCodeAt(i) === 0x20 || value.charCodeAt(i) === 0x09)
const charCode = value.charCodeAt(start)
if (charCode !== 0x20 && charCode !== 0x09) {
break
}
start++
}
while (end > start) {
//@ invariant start >= 0 && start <= end && end <= value.length
//@ invariant forall(i: int, i >= 0 && i < start ==> value.charCodeAt(i) === 0x20 || value.charCodeAt(i) === 0x09)
//@ invariant forall(i: int, i >= end && i < value.length ==> value.charCodeAt(i) === 0x20 || value.charCodeAt(i) === 0x09)
const charCode = value.charCodeAt(end - 1)
if (charCode !== 0x20 && charCode !== 0x09) {
break
}
end--
}
//@ assert value.slice(0, value.length) === value
return start === 0 && end === value.length ? value : value.slice(start, end)
}
```
相关文件：
- TypeScript 版 [`trimCookieWhitespace`](https://github.com/midspiral/hono-lemmascript/blob/lemmascript/src/utils/cookie.ts#L79-L112)
- LemmaScript 生成的 Dafny 版 [`trimCookieWhitespace`](https://github.com/midspiral/hono-lemmascript/blob/lemmascript/src/utils/cookie.dfy)
## 示例：绿地场景——游戏决策过程的完备性与可靠性验证
“Equality” 是一款小游戏：双方各持 1–9 的数字牌，目标是通过四则运算（`+`、`-`、`*`、`/` 仅当整除时）让两边结果相等。
在 Dafny 中，我们定义幽灵谓词 `ExpressionsAgree(L: seq, R: seq)`，断言存在表达式 `eL` 与 `eR`，其叶子节点各自与 `L`、`R` 作为多重集相等，且求值结果相同。
借此可证明 UI 调用的 `canEqualize` 既可靠（返回 `true` 时必存在解）又完备（返回 `false` 时必无解）。
```dafny
ghost predicate ExpressionsAgree(L: seq, R: seq) {
exists eL: Expr, eR: Expr ::
multiset(leaves(eL)) == multiset(L) &&
multiset(leaves(eR)) == multiset(R) &&
evalExpr(eL).ok? && evalExpr(eR).ok? &&
evalExpr(eL).v == evalExpr(eR).v
}
method canEqualize(L: seq, R: seq) returns (res: bool)
requires (|L| >= 1)
requires (|R| >= 1)
ensures res <==> ExpressionsAgree(L, R)
```
相关文件：
- TypeScript 版 [`canEqualize`](https://github.com/midspiral/equality-game-lemmascript/blob/main/src/equality.ts#L79-L83)
- Dafny 版 [`canEqualize`](https://github.com/midspiral/equality-game-lemmascript/blob/main/src/equality.dfy#L809-L812)（位于 LemmaScript 生成的脚手架文件顶部）
## 展望
目前已有的[案例研究](https://github.com/midspiral/lemmascript#examples-and-case-studies)不断拓展 LemmaScript 的能力边界。我们欢迎你将其用于绿地或棕地项目，同时请注意：
- 不同项目可能仍需对验证工具链进行定制，例如支持新的 TypeScript 语法或特性
- 尽管验证模型系统性地源自 TypeScript 源码，语义仍可能存在偏差；建议引入差分测试以增强信心
- 棕地项目的就地验证往往更具挑战，因为原始代码并未考虑验证需求
抛开这些注意事项，LemmaScript 已在发现问题与确认代码正确性方面显现价值。
关于使用场景，绿地与棕地的差异也暗示了一条路线图：
- 绿地项目——从一开始就融入验证友好设计（类似 `dafny-replay` 模式：先定义状态不变式，再确保每个 UI 动作都保持该不变式）
- 棕地项目——选择性对关键组件进行就地验证，或在安全修复时做“验证式重写”，让修复不仅“声称”解决安全问题，更能“证明”其正确性
相似文章
Vercel 发布 Scriptc：TypeScript 到原生代码编译器，二进制文件不包含 JavaScript 引擎
Vercel Labs 发布了 Scriptc，这是一款编译器，能将普通 TypeScript 代码转换为小巧、快速的原生可执行文件，无需在二进制文件中包含 Node、V8 或任何 JavaScript 引擎。它支持 TypeScript 的大部分静态特性及 Node 的 API 接口。
microsoft/TypeScript
TypeScript 是一种用于大规模 JavaScript 应用的语言，它增加了可选类型。该仓库托管了 TypeScript 编译器及相关工具。
# 结合语义等价自博弈与形式化验证提升 LLM 代码推理能力
爱丁堡大学研究人员提出了一种利用 Liquid Haskell 进行形式化验证的自博弈框架，用于训练 LLMs 的语义等价推理能力，同步发布了 OpInstruct-HSx 数据集（28k 个程序），并在 EquiBench 上实现了 13.3 个百分点的准确率提升。
Specula：扩展形式化规范以实现系统代码的自主模型检查（13分钟阅读）
Specula是一个代理系统，能够自动从代码推导TLA+规范，运行模型检查以发现并发错误，并通过集成测试复现这些错误。它在48个开源分布式和并发系统中发现了249个错误，展示了形式化验证的显著扩展。
VeryTrace：通过可编译形式化与结构化验证来验证推理轨迹
VeryTrace 是一种零样本验证与修复框架，它将大语言模型的推理轨迹通过领域特定语言形式化为可编译表示，从而通过确定性检查与大语言模型审计的混合方式实现步骤级错误定位。该框架在数学、机器人学和关系推理等多个领域提升了准确性，且无需领域特定训练。