Valen 编程语言是一个旨在提供内存安全的可变别名（mutable aliasing）的实验性项目，它正在实现一种通过反向遍历函数来运行的借用检查器。虽然大多数编译器和借用检查器（例如 Rust 或 Vale 中的）执行正向扫描来确定区域推断或安全性，但 Valen 的架构从函数的最后一条语句处理到开头。这种反转旨在解决内存安全中的特定技术障碍，特别是关于识别变量的最后使用点以及基于循环的失效复杂性问题。
该机制依赖于多阶段的编译过程。在将源代码解析为抽象语法树（AST）并执行静态类型检查后，编译器执行“静态分组”。此阶段确定引用指向变量或数据结构的确切部分，有效地将“路径”信息嵌入到变量的类型中。在最终的安全检查阶段，编译器执行反向扫描。它维护一个“待处理”列表，包含在函数后续位置使用的变量。当扫描遇到“USE”事件时，该变量被添加到待处理列表中。当它遇到“MUTATE”事件时，编译器会检查待处理列表中的变量是否因该变动而失效。如果变动影响了待处理变量，编译器将标记 use-after-free 错误。这允许编译器立即识别冲突，因为它已经知道哪些变量必须保持有效直到函数结束。
采用这种反向方法的主要动机之一是处理循环并避免复杂的“获取并导航”操作。在正向扫描中，如果最后一次使用嵌套在循环中，或者需要向前查看以确定变量是否会被后续赋值“复活”，那么识别变量的最后一次使用可能会变得困难。反向扫描自然地首先识别最近的一次使用，从而简化了确定变量是否仍然有效的账目记录。然而，这种方法也面临自身的挑战，例如在为不同的证明目标多次扫描代码时如何保持性能。通过摆脱 Rust 等语言中使用的约束求解模型，Valen 寻求一种更符合语法的算法，在保持与 Rust 生态系统兼容的同时简化内存安全规则。