摘要
Python 已成为通用编程的主导语言，但其在形式化验证方面仍缺乏强有力的工具支持。相比之下，使用 C 等语言的程序员可以借助成熟的模型检测工具（如 CBMC），实现全面的符号推理与错误定位。然而，Python 语言本身的复杂性，以及现有转译工具（如 Cython）在语法冗长性和低级特性方面的局限，长期以来制约了形式化验证在 Python 程序中的应用。本文提出 PyVeritas，一种新型框架，该框架利用大语言模型（Large Language Models, LLMs）实现从 Python 到 C 的高层级转译，随后对生成的 C 代码进行有界模型检测（bounded model checking）以及基于 MaxSAT 的错误定位。PyVeritas 使得原本针对 C 语言的模型检测工具能够用于 Python 代码的形式化验证与缺陷定位。我们在两个 Python 基准测试上的实证评估表明，基于大语言模型的转译方法可达到较高的准确率，部分 LLM 的准确率高达 80%–90%，从而构建出一个有效的开发环境，支持基于断言的验证机制，并为小型但非平凡的 Python 程序提供可解释的故障诊断能力。