VeriPy: Source-Preserving Verification and Compatibility Checking for Python Components¶

会议: NeurIPS 2026
arXiv: 2610.02814
代码: https://github.com/astrio-labs/veripy
领域: 代码智能
关键词: 形式化验证, 软件向后兼容性, Python组件验证, 关系验证, 源代码保留

一句话总结¶

VeriPy 通过行内 #@ 注解、类型化准入网关与 Dafny/Lean 双后端编码器，在完整保留 Python 原生可执行代码的前提下实现函数正确性验证，并通过关系积程序判定组件版本升级间的向后兼容性。

研究背景与动机¶

在现代软件工程中，保持动态语言程序与其形式化规范之间的一致性是一项艰巨的长期维护挑战。以 Python 为代表的动态语言广泛应用于系统后端与科学计算，但其缺乏静态约束和隐式行为极易导致缺陷。现有程序验证工具如 Frama-C（针对 C 语言）或 Nagini（针对 Python 并编译到 Viper 中间语言）虽然证明了源码级规范的价值，但在演进维护场景下仍面临两大根本断层：其一，验证系统往往要求对代码进行侵入式改写或剥离底层执行环境，使得经证明的模型与实际运行的 Python 组件脱节；其二，传统单版本函数验证无法保障向后兼容性，即使新版本实现完全满足相同的前后置范围契约，它对已有调用方暴露的具体行为（如返回值与异常分支）仍可能发生静默漂移。

这种维护断层的核心矛盾在于：单一版本的弱后置条件（如范围约束或布尔属性）无法约束版本更替时的确定性一致，而重写算法（例如 Django int_to_base36 从左至右编码改为 divmod 倒序拼接）在结构上存在巨大差异，静态验证器极难推断任意循环之间的对齐关系。若依赖全量自动化重推导，庞大的状态空间与环境依赖模型往往导致求解器超时或误报；若缺乏严谨的关系验证语义，版本升级就只能依赖有限测试用例盲目兜底。

本文的切入角度是将 Python 组件本身作为面向开发者的基本验证单元，把单版本函数验证与跨版本关系验证统一到同一个轻量化工作流中。核心 idea：通过无侵入的 #@ 源码注释定义契约与循环不变量，利用类型化准入网关与显式依赖模型直接将原版 AST 编码至 Dafny/Lean 双后端，并构造顺序关系积程序（Relational Product）直接形式化证明旧输入集在新版本上的全接纳性以及返回值与异常标签的观测等价性。

方法详解¶

整体框架¶

VeriPy 将 Python 函数组件作为统一的开发者交互单元，其完整流水线涵盖静态准入检查、规范转译、双后端形式化求解、运行时防护包装以及跨版本关系验证。整体处理流程如下：首先接收包含 #@ 注解的 Python 原生组件与显式环境声明，经由 basedpyright 严格静态类型检查后，通过结构准入网关（Admission Gate）过滤未建模的动态特性（如类反射或任意正则）；随后由 Dafny 或 Lean 的专用 AST 编码器将程序、辅助引理（Checked Sidecars）及依赖快照编译为验证命题；在跨版本维护时，系统自动构建双版本顺序关系积程序，由求解器一次性验证两个函数体及其关系引理，输出四类互斥判决结果。

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["Python 组件与 #@ 契约注解"] --> B["静态类型与结构准入网关<br/>basedpyright + 显式环境模型"]
    B --> C["双后端直接 AST 编码<br/>Dafny SMT 与 Lean 内核证明"]
    C --> D["顺序关系积程序构造<br/>双版本命名空间隔离与契约绑定"]
    D --> E["兼容性与正确性判定判决<br/>Proved / Witness / Inconclusive / Unsupported"]
    E --> F["运行时保护层代码生成<br/>输入前置断言与不可变快照守卫"]

关键设计¶

1. 源码保留的契约规范与辅助引理侧车机制

为了彻底避免形式化规范对生产代码的污染与侵入，VeriPy 将所有前后置条件（ensures）、循环不变量（invariant）、终止度量（decreases）与证明挂钩（proof）均置于原生 Python 的 #@ 注释内。在 CPython 运行时环境下，这些注释被完全忽略，原生组件以零运行时开销保持原始字节流执行。对于复杂归纳证明所需的数学引理，VeriPy 引入了外置的辅助验证侧车（Checked Sidecars），例如在递归编码定义与循环推进之间建立联系的幽灵谓词（Ghost Predicates）： $$\mathit{ExactEncoding}(n, s) \equiv n \ge 0 \land s = \mathcal{D}(n)$$ 其中 $\mathcal{D}(n)$ 表示规范基数编码。开发者或 LLM 代理通过源代码行号映射的诊断反馈不断细化这些侧车引理，严禁在后端侧车中注入破坏可靠性的任意公理假定（Axiomatic Additions），确保所有定理严格闭合。

2. 基于 Dafny 与 Lean 的直接 AST 编码及严苛信任边界

系统不依赖通用的后端中立中间语言（IR），而是实现了两套直接针对 Dafny（基于 SMT 自动化求解）与 Lean 4（内核交互式证明验证）的 AST 编码器。该设计针对 Python 运行语义设立了严格的显式环境模型：模块级全局常量通过有界 AST 解释器求值确定；字符串操作限定为 Unicode 标量且在边界拒绝孤立代理对（Lone Surrogates）；复杂对象通过只读字段快照（Snapshots）隔离，排除了属性描述符、动态反射与并发修改。两套后端独立构建不仅实现了跨求解机制的双重校验，还通过审计规则拦截了诸如在 Lean 侧车中声明 False 类型全局假设而导致的前端虚假证明漏洞。

3. 作用域向后兼容性检验的关系积程序构造

在组件版本升级时，单函数验证无法防止行为突变。VeriPy 针对旧版本 $v_{\text{old}}$ 与新版本 $v_{\text{new}}$ 的输入准入契约 $A_v(x)$ 和映射模型 $M_v(x)$，将向后兼容性形式化为全称量化关系命题： $$\forall x.\ A_{\text{old}}(x) \Longrightarrow \bigl(A_{\text{new}}(x) \land \mathcal{O}(M_{\text{old}}(x)) = \mathcal{O}(M_{\text{new}}(x))\bigr)$$ 其中观测算子 $\mathcal{O}$ 严格投影到类型化返回值与建模异常标签（如 ValueError、InvalidName）。VeriPy 将新旧两版代码置于独立命名空间，并串联构造顺序关系积程序（Relational Product），通过两端的精准函数契约与归纳关系引理将关系判定规约为标准单体程序验证。系统严格报告四类判决边界：Proved（完成积程序封闭形式证明）、Counterexample（通过原生执行重放发现实质观测分歧的反例证据）、Inconclusive（已准入但证明超时且无反例证人）、Unsupported（超出当前抽象语法与环境支持范围），绝不将证明超时混淆为兼容性破坏。

一个完整示例¶

以 Django 的 int_to_base36 算法重写为例：旧算法（Django 历史版本）先使用循环递增幂次确定最高位因子，再由高位向低位逐位截取字符；新算法则采用 divmod(i, 36) 由低位向高位生成余数并向头部拼接字符串。两者的循环执行轨迹完全不对齐。

在 VeriPy 中，两者共享统一的高层幽灵契约 $\mathit{ExactEncoding}(\mathrm{old}(i), \mathrm{result})$。旧版通过循环不变量 LeadingProgress(old(i), i, factor, base36) 跟踪高位前缀生成，并在循环内部注入引理挂钩 #@ proof StartEncoding(i, factor) 与 #@ proof PythonLeadingStep(...)；新版则通过 EncodingProgress(old(i), i, b36) 并在 divmod 前调用 #@ proof EncodingStep(...)。VeriPy 构造的关系积程序引入两者到统一验证上下文中：对任意输入整数 $i$，当满足 $i \ge 0$ 时，旧版与新版分别通过归纳引理证明其返回值均等于基数规范定义 $\mathcal{D}(i)$，从而在 Dafny 中以 267 条验证义务全数自动闭合证明了新旧两套截然不同的循环实现完全向后等价；对于负数输入 $i < 0$，关系积程序则证明两者必然抛出完全同构的 ValueError 异常标签。

实验关键数据¶

主实验¶

论文在 Ubuntu CI 验证矩阵中对来自 7 个知名开源库（包含 Black、SGLang、PyTorch、Django、vLLM、CPython、python-stdnum）的 25 个双后端配对组件单元进行了验证，所有单元均在 Dafny 4.11.0 与 Lean 4.33.1 下通过全量形式化求解（共 50 次完整证明调用）。

评估组件	代码量 (Py / Spec / Hint LOC)	Dafny 侧车行数 / 耗时 (s)	Lean 侧车行数 / 耗时 (s)	形式化证明属性
Black 范围组合	98 / 8 / 19	119 / 8.98s	421 / 12.48s	精确有序输出与边界契约
SGLang 动态规划器	27 / 12 / 14	79 / 6.36s	125 / 7.15s	内存长度界限与预留约束
PyTorch 分片重叠验证	94 / 18 / 27	357 / 22.66s	1759 / 110.76s	多维分片重叠检测与异常类
Django base36 编码	11 / 2 / 7	27 / 5.37s	106 / 6.84s	严格十进制至36进制字符及异常
vLLM 补齐优化器	17 / 6 / 6	0 / 5.42s	266 / 12.21s	最优对齐解与平局打破规则
CPython 时间解析器	37 / 34 / 0	0 / 12.73s	976 / 163.59s	34项格式字段与异常映射
Luhn 校验和	7 / 4 / 1	67 / 4.16s	70 / 1.83s	严格十进制校验累加和
Luhn 校验位计算	13 / 12 / 2	120 / 7.49s	260 / 2.14s	编解码十进制可逆往返属性
Luhn 完整验证	26 / 13 / 0	0 / 3.20s	59 / 2.36s	综合数值上下界与错误类型

在 10 个固定开源仓库历史演进边界的向后兼容性检验中，系统准确判定了四类不同行为：

目标代码库	被选定组件接口	代码是否变更	判定判决 (Verdict)	关键结论与证人说明
Black	`is_valid_line_range`	是 (Yes)	Proved	证明冗余空检查消除后的输入输出等价
Django	`int_to_base36`	是 (Yes)	Proved	成功证明两套不同循环算法的向后兼容
CPython	`_days_before_year`	否 (No)	Proved	基线控制组，证明无变更函数自反兼容
Werkzeug	`quote_etag`	否 (No)	Proved	基线控制组，成功验证默认参数等价
Packaging	`canonicalize_name`	是 (Yes)	Counterexample	捕获 3 个实质不兼容证人（如换行符引发 `InvalidName`）
python-stdnum	`checksum`	否 (No)	Inconclusive	弱契约无法约束任意字符映射，证明未闭合
PyPNG	`undo_filter_paeth`	否 (No)	Unsupported	涉及可变缓冲区原地修改与别名操作，超出当前范围
SGLang	`page_aligned_decode_alloc_lens`	否 (No)	Unsupported	早期快照缺乏记录类型支持（后续扩展中证明）
PyTorch	`_check_shard_metadata_pair_overlap`	否 (No)	Unsupported	早期缺乏结构体快照支持（后续扩展中证明）
vLLM	`_approximate_gcd`	否 (No)	Unsupported	缺少可选参数/可变默认值边界支持

关键发现¶

历史代码重构与语义断裂识别：在 Packaging 的 canonicalize_name 比较中，工具准确识别出新版本增加了输入校验导致 name="foo\n" 从直接返回转变为抛出 InvalidName 异常，同时更早将大写转为小写导致希腊字母最终 sigma 的替换行为发生改变，给出了明确的反例输入证人（Concrete Witnesses）。
语言后端证明代价特征差异明显：对于相同的 Python 语义，Dafny 依赖 SMT 自动求解在多数中等逻辑中侧车编写开销极小（如 CPython time parser 和 vLLM padding 为 0 行侧车）；而 Lean 4 依赖内核严格证明，相同任务需要编写庞大的辅助引理库（如 CPython time parser 需要 976 行非注释非空 Lean 侧车，PyTorch 需要 1759 行）。
旧证明复用（Proof Reuse）的有效性归因：在 48 组基于 LLM（GPT-6-Astra）的维护代码生成实验中，复用旧证明使联合成功率从 41.7%（Rebuild）提高至 58.3%（Reuse）。然而消融诊断显示，这一差距的核心主要来自于旧证明中暴露了后端正则等库 API 的定义；一旦向两方均提供公开库环境定义，两者均能 100% 在单轮内完成证明，说明当前代码维护的核心瓶颈在于显式环境信息的对齐。

亮点与洞察¶

零侵入保留原生 Python 代码：将断言、不变式与引理全部内嵌于 #@ 行内注释，既保持了与 CPython 生态的纯原生兼容，又实现了精确到源码行号的证明错误回传。
关系积程序攻克循环重构难题：无需通过启发式规则去猜测甚至强行对齐两个版本间完全不同的控制流与循环结构，而是通过外部函数契约与自闭合的归纳侧车在积程序中完成了算法重写间的语义等价性判定。
严谨的四元判决体系：严格区分证明成功、反例证人、超时未决与语言未受支持边界，避免了将验证器能力的局限错误地视作代码存在向后不兼容缺陷。

局限与展望¶

动态语言语义覆盖受限：目前系统不支持任意 Python 类继承、动态属性反射、可变内存缓冲区的关系验证（如 PyPNG）以及复杂的并发与异常回溯信息比较。
对严苛类型提示的强依赖：代码必须能够通过 strict basedpyright 检查，在真实历史回溯实验中，大量历史提交因为缺少局部类型标注或存在动态调用而在提取阶段即被拦截。
未来方向：拓展对内存原地别名修改（In-place Buffer Mutation）的关系验证模型，并结合自动化符号执行工具提升复杂对象契约与不变量的自动推导能力。

评分¶

新颖性: ⭐⭐⭐⭐☆ 创新性地将源码注释规范、双定理证明器后端与跨版本关系积程序融合于 Python 组件级维护中。
实验充分度: ⭐⭐⭐⭐⭐ 涵盖 7 个代表性开源库的 25 个双后端验证单元、10 个真实历史兼容性演进案例以及严格的 LLM 辅助维护消融。
写作质量: ⭐⭐⭐⭐⭐ 概念界定极其清晰，对证明局限、环境假设与反例证人展开了不偏不倚的坦诚剖析。
价值: ⭐⭐⭐⭐☆ 为动态语言核心算法与基础库的高可靠演化及形式化自动化维护提供了极具参考价值的工程落地路径。