发表机构
Astrio Labs（Astrio实验室）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
VeriPy提出一种统一工作流，通过注释表达契约并生成Dafny/Lean工件，实现Python组件的源级验证与向后兼容性检查。
AI 中文摘要
保持Python程序与其形式化保证的一致性是一个持续性的维护问题。规格说明必须描述实际运行的实现，且更新必须保留现有调用方所依赖的行为。VeriPy将这些义务整合到一个针对带注解Python组件的统一工作流中。开发者和智能体将契约、不变量和证明钩子表达为Python注释，然后利用源定位的诊断信息来细化经过检查的辅助引理。直接编码器生成Dafny或Lean工件，同时保留可执行的函数体及其依赖的显式模型。一个关系型产品检查更新后的组件是否仍接受旧输入，并保留返回值及建模的异常。由此产生的工作流将源代码级别的证明开发与功能验证和向后兼容性检查相连接，并记录了每项保证适用的假设条件。代码可在该https URL获取。
英文摘要
Keeping a Python program and its formal guarantees aligned is a continuing maintenance problem. Specifications must describe the implementation that actually runs, and updates must preserve the behavior on which existing callers depend. VeriPy brings these obligations into a common workflow for annotated Python components. Developers and agents express contracts, invariants, and proof hooks as Python comments, then refine checked auxiliary lemmas using source-located diagnostics. Direct encoders produce Dafny or Lean artifacts while retaining admitted executable bodies and explicit models of their dependencies. A relational product checks whether an updated component still admits old inputs and preserves returned values and modeled exceptions. The resulting workflow connects source-level proof development with functional verification and backward compatibility, recording the assumptions under which each guarantee applies. The code is available at https://github.com/astrio-labs/veripy.
CommentsAccepted to NeurIPS 2026 VeriCodeGen
