一句话：提出 Lawyer，首个支持模块化高阶非直谓活性规约的机械化程序逻辑，用纯逻辑标记迁移系统嵌入义务，避免辅助代码插桩。
高阶并发分离逻辑（如 Iris）擅长验证并发程序的安全性，但其活性（公平终止）验证要么缺乏模块化，要么难以机械化。本文提出 Lawyer：一个模块化验证并发程序（公平）终止的机械化程序逻辑。它借鉴基于义务（obligation）的终止证明方法，但不插桩辅助代码，而是将义务嵌入纯逻辑的标记迁移系统，并证明程序精化该系统，因而更易机械化。作者验证了多个实例，包括终止性依赖公平锁库正确性的客户端程序的模块化验证，以及单独证明票据锁实现满足该库接口。据作者所知，Lawyer 是首个支持模块化高阶非直谓活性规约的机械化程序逻辑，结果均已在 Rocq 中基于 Iris 机械化。
Higher-order concurrent separation logics, such as Iris, have been tremendously successful in verifying safety properties of concurrent programs. However, state-of-the-art attempts to verify liveness properties in such logics have so far either lacked modularity (the ability to compose specifications of independent modules), or they have been far too complex to mechanize in a proof assistant. In this work, we introduce Lawyer — a mechanized program logic for modular verification of (fair) termination of concurrent programs. Lawyer draws inspiration from state-of-the-art approaches that use obligations for specifying and proving termination. However, unlike these approaches, which incorporate obligations by instrumenting the source code with erasable auxiliary code and state, Lawyer avoids such instrumentations. Instead, Lawyer incorporates obligations into the logic by embedding them into a purely logical labeled transition system that the program is shown to refine — this makes Lawyer far more amenable to mechanization. We demonstrate the expressivity of Lawyer by verifying termination of a range of examples, including modular verification of a client program whose termination relies on correctness of a fair lock library, and (separately) proving that a ticket lock implementation implements that library’s interface. To the best of our knowledge, Lawyer is the first mechanized program logic that supports modular higher-order impredicative liveness specifications of program modules. All the results that appear in the paper have been mechanized in the Rocq proof assistant on top of the Iris separation logic framework.
@article{paperbot3830,
title = {Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic},
author = {Egor Namakonov and Justus Fasse and Bart Jacobs and Lars Birkedal and Amin Timany},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798240}
}