一句话：提出基于 Lean 的框架，用 monad transformer 代数自动导出可靠的验证条件生成器，以构建有根基的多模态程序验证器。
多模态程序验证结合动态与符号技术，并用自动化与交互式工具证明代码符合规约；但这类工具自身也需可靠，即带有形式化的可靠性证明（foundational）。本文提出一个便于构建既有根基又多模态的验证器的框架。其思路是将可执行程序语义以 monad 浅嵌入方式嵌入到基于高阶逻辑的定理证明器（Lean）中，并提供 monad transformer 库来编码状态、发散、异常与非确定性等计算效应。核心理论创新是 monad transformer 代数，可自动导出相应可靠的验证条件生成器。生成的验证条件既可由现成 SMT 求解器自动证明，也可在自动化失败时转为交互式证明。作者将该框架实例化为两个嵌入 Lean 的有根基多模态验证器，分别处理分布式协议安全性与 Dafny 风格的命令式程序规约，并机器化验证了多个非平凡案例。
Multi-modal program verification is a process of validating code against its specification using both dynamic and symbolic techniques, and proving its correctness by a combination of automated and interactive machine-assisted tools. In order to be trustworthy, such verification tools must themselves come with formal soundness proofs, establishing that any program verified in them against a certain specification does not violate the specification’s statement when executed. Verification tools that are proven sound in a general-purpose proof assistant with a small trusted core are commonly referred to as foundational . We present a framework that facilitates and streamlines construction of program verifiers that are both foundational and multi-modal. Our approach adopts the well-known idea of monadic shallow embedding of an executable program semantics into the programming language of a theorem prover based on higher-order logic, in our case, the Lean proof assistant. We provide a library of monad transformers for such semantics, encoding a variety of computational effects, including state, divergence, exceptions, and non-determinism. The key theoretical innovation of our work are monad transformer algebras that enable automated derivation of the respective sound verification condition generators. We show that proofs of the resulting verification conditions enjoy automation using off-the-shelf SMT solvers and allow for an interactive proof mode when automation fails. To demonstrate versatility of our framework, we instantiated it to embed two foundational multi-modal verifiers into Lean for reasoning about (1) distributed protocol safety and (2) Dafny-style specifications of imperative programs, and used them to mechanically verify a number of non-trivial case studies.
@article{GladshteinPZKS26,
title = {Foundational Multi-Modal Program Verifiers},
author = {Vladimir Gladshtein and George Pîrlea and Qiyuan Zhao and Vitaly Kurin and Ilya Sergey},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776719}
}