一句话：提出以正则表达式跟踪访问路径的借用检查类型系统，经 Lean 机械化并部署于 Sui 的 Move 字节码验证器。
Rust 等安全系统语言通过所有权与借用检查在编译期防止悬垂引用和数据竞争，而 Move 智能合约语言虽采用该模型，却将引用限制为以局部变量为根的结构化访问路径，从而免去生命周期标注。本文为 Move 借用检查器提出一种新类型系统，用正则表达式跟踪访问路径：Brzozowski 导数刻画借用操作的可达性后果，Kleene 星概括函数调用与循环产生的借用链，别名检查归约为可判定的正则表达式空性判定，该设计可自然扩展到向量与枚举类型。该借用检查器已实现于 Sui 区块链的 Move 字节码验证器中，取代原有借用分析器并保持完全向后兼容。作者还在 Lean 中机械化该类型系统，给出机器检查的可靠性证明，并将可执行算法类型检查器与生产 Move 编译器对测；这套约 39,000 行的元理论借助 AI 证明助手在约一个月内完成，是迄今规模最大的 AI 辅助 PL 元理论机械化之一。
Safe systems languages such as Rust enforce an ownership discipline through types: every value has a unique owner, and the type system tracks borrows—references that provide temporary access to values without transferring their ownership. Borrow checking is a static analysis ensuring that no borrow outlives its owner and that no two mutable borrows are aliases, preventing dangling references and data races at compile time. Move, a smart contract language deployed on Sui and Aptos blockchains, adopts this model but restricts references to structured access paths rooted in local variables, eliminating the need for complex lifetime tracking mechanisms such as lifetime annotations. We present a novel type system for Move's borrow checker in which access paths are tracked by regular expressions. In this model, Brzozowski derivatives make it possible to express the reachability consequences of borrowing operations, Kleene star summarises borrow chains from function calls and loops, and the aliasing check reduces to the decidable regex emptiness. The design of the type system with regular expression-based borrow tracking extends naturally to vectors and enumeration types. The proposed design of a borrow checker has been implemented in the Move bytecode verifier for Sui blockchain, where it superseded the original borrow analyser while maintaining full backwards compatibility. We mechanised the type system in Lean with a machine-checked soundness proof and an executable algorithmic type checker tested against the production Move compiler. Notably, this 39,000-line metatheory was developed with an AI proof assistant in roughly one month, and we report on our experience of conducting this proof effort, which is among the largest AI-assisted PL metatheory mechanisations to date.
@article{paperbot12133,
title = {Tracking Borrows with Regular Expressions},
author = {Todd Nowacki and Sam Blackshear and John Mitchell and Shaz Qadeer and Ilya Sergey},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839521}
}