一句话：首个经机器化验证、忠实于 ECMAScript 规范的回溯正则语义，并用于重写等价与 PikeVM 证明。
现代 JavaScript 正则表达式采用回溯语义，但此前缺乏既简洁实用、又经机器化证明忠实于 ECMAScript 规范的完整语义。本文在 Rocq 证明助手中给出首个这样的语义，通过证明其与既有 ECMAScript 规范逐行嵌入等价来保证忠实性；与规范及其他形式化工作不同，它捕获的不是仅最高优先级的匹配，而是记录所有可能匹配及其优先级的完整回溯树。作者展示两项实际应用：为现代正则提出上下文等价概念，据此证明或反驳既有工作给出的重写规则；并给出许多真实引擎所用 PikeVM 算法的首个形式化证明。全部定义与结果均已在 Rocq 中机器化。
We present the first mechanized, succinct, practical, complete, and proven-faithful semantics for a modern regular expression language with backtracking semantics. We ensure its faithfulness by proving it equivalent to a preexisting line-by-line embedding of the official ECMAScript specification of JavaScript regular expressions. We demonstrate its practicality by presenting two real-world applications. First, a new notion of contextual equivalence for modern regular expressions, which we use to prove or disprove rewrites drawn from previous work. Second, the first formal proof of the PikeVM algorithm used in many real-world engines. In contrast with the specification and other formalization work, our semantics captures not only the top-priority match, but a full backtracking tree recording all possible matches and their respective priority. All our definitions and results have been mechanized in the Rocq proof assistant.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BarriereDP26,
title = {Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications},
author = {Aurèle Barrière and Victor Deng and Clément Pit-Claudel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776710}
}