跳到正文
Hacker News· carnevalem·· 2 天前AI 评分74

用 AI 智能体将 CPython 形式化为 Lean 模型，发现 418 个 Python bug

Formalizing CPython

AI 导读

研究团队用 Opus 5.5 智能体把 CPython 3.15.2 的函数逐行改写为 Lean，经测试、证明和独立审查后，已完成 4,071 个函数，产出 613,318 行 Lean 代码、18,898 条定理与引理。

正文 · AI 翻译

AI 智能体编写了 613,318 行 Lean 代码，逐行复制了 Python 的内部实现，将每一部分都与真实的 Python 进行测试，让计算机检查了每一个证明，并在此过程中发现了 418 个 Python 缺陷报告。

CPython · Objects/rangeobject.c

static unsigned longget_len_of_range(long lo, long hi, long step){    assert(step != 0);    if (step > 0 && lo < hi)        return 1UL + (hi - 1UL - lo) / step;    else if (step < 0 && lo > hi)        return 1UL + (lo - 1UL - hi) / (0UL - step);    else        return 0UL;}

Lean 副本 · RangeSlice/Model.lean

def getLenOfRange (lo hi step : Int) : Int :=  if step > 0 ∧ lo < hi then    uadd 1 (usub (usub (toU hi) 1) (toU lo) / toU step)  else if step < 0 ∧ lo > hi then    uadd 1 (usub (usub (toU lo) 1) (toU hi)              / usub 0 (toU step))  else 0 -- step ≠ 0 is assumed by every proof-- uadd, usub: C's unsigned arithmetic,-- which wraps around past 2^64
左侧是 CPython C 源代码中的一个函数，右侧是智能体编写的 Lean 副本。将鼠标悬停在某一行上即可查看其对应行。

简而言之

  • 我们将 Opus 5.5 指向 CPython——运行几乎所有 Python 代码的程序——让它用 Lean 重写其函数，Lean 是一种用于编写机器可检查证明的语言。
  • 每次重写都逐行复制原始代码，并在任何人尝试对其证明任何东西之前，用数万个输入与真实 Python 进行测试。
  • 只有当另一个未参与编写的智能体检查工作并认可其成立时，一个函数才算数。到目前为止，已有 4,071 个函数通过了该检查。
  • 结果是 1,539 个文件中共 613,318 行 Lean 代码，包含 18,898 个定理和引理，全部在每次构建时由 Lean 的证明检查器检查。
  • 在此过程中，这些证明产生了 418 个缺陷报告。大多数很小，但约有 55 个可以从普通 Python 代码导致解释器崩溃或内存损坏。

已检查并接受已编写，尚未接受未开始

  • 整个 CPython16%
  • 解释器核心10%
  • 内置类型35%
  • C 模块19%
  • 解析器31%
  • 语法规则100%
  • 标准库9%
CPython 3.15.2 的每个部分有多少已被复制、测试、证明并通过审查接受。没有可检查内容的代码，例如内存记账，被排除在外。

为什么要费这个劲

Python 没有精确的书面定义。有一份参考手册，但实际上“Python”意味着 CPython 所做的任何事情，而 CPython 是数十万行 C 代码加上一个大型标准库。手册涵盖了正常使用情况。它对奇怪的情况着墨甚少，而缺陷恰恰藏在那里：一个对象在字典搜索它时改变了该字典，更新进行到一半时抛出的错误，比 C 代码编写时针对的最大值还大一的数字。

为一个函数编写证明迫使你准确说明它在所有这些情况下的行为。你不能留下任何模糊之处，因为证明检查器不会接受。这使得证明成为发现代码未按所有人假设行事之处的好方法。

我们想看看在像 CPython 这样庞大而古老的代码库上这能走多远，以及当大部分工作由 AI 完成时结果是否仍然可信。

工作原理

每个函数都经过相同的四个步骤。

  1. 复制用 Lean 重写该函数，逐行遵循原始代码，包括其错误消息和其奇怪角落。
  2. 测试在至少 50,000 个棘手输入上并排运行副本和真实 Python。任何不一致都意味着副本有误。
  3. 证明陈述应该始终为真的事情，并让计算机检查证明。如果它实际上是假的，就证明相反的情况。
  4. 检查另一个未参与工作的智能体对照原始代码审查它并试图打破它。只有幸存下来的才算数。

本页顶部的代码是 CPython 一小部分的第一步：这个 C 函数负责算出一个 range 里有多少个数字，旁边是它的 Lean 副本。该副本保留了 C 代码的精确算术，包括数字过大时如何回绕。关于它的证明表明，这个函数、CPython 用于超大数字的较慢版本，以及二者之间的选择代码，始终给出相同且正确的计数。

什么也没证明的证明

最难的部分不是让 AI 智能体写证明，而是让证明真正有意义。

我们第一次尝试要求智能体追求广度：复制每个函数，并至少为每个函数证明一件事。它们做到了。随后一次独立审查发现，它检查的函数中不到一半站得住脚，有一个文件里只有 21%。这些证明全都正确，只是没说明任何有用的东西。例如，“如果这个函数返回一个数字，该数字至少为零”是真的，但一个总是崩溃的函数也满足它。

因此，审查者现在对每个证明只问一个问题：函数的错误版本是否也能通过它？

函数版本“如果它返回，答案 ≥ 0”“它总是返回正确的计数”
真实版本通过通过
总是崩溃通过被抓住
对超大数字返回 0通过被抓住
倒计数时差一通过被抓住
关于同一函数的两个真陈述。第一个让所有错误版本都能通过，所以一个只有这种证明的函数不算数。

修复弱证明通常意味着回头把副本做得更真实，例如让用户代码在函数中途抛出错误。下面的图表展示了十个文件的情况。每个点是一轮审查。线条有时会下降：当审查者发现一个已接受的证明对真实 Python 来说是错的，所有依赖它的内容都会被撤回。

已接受的函数

Objects/typeobject.c142 个中的 135 个已接受 · 5 轮审查
Objects/genobject.c56 个中的 56 个已接受 · 5 轮审查
Objects/setobject.c46 个中的 46 个已接受 · 7 轮审查
Modules/_json.c48 个中的 45 个已接受 · 5 轮审查
Lib/enum.py39 个中的 37 个已接受 · 9 轮审查
Lib/random.py38 个中的 37 个已接受 · 3 轮审查
Objects/abstract.c43 个中的 41 个已接受 · 2 轮审查
Objects/rangeobject.c33 个中的 33 个已接受 · 2 轮审查
Lib/pickletools.py33 个中的 31 个已接受 · 2 轮审查
Modules/binascii.c40 个中的 35 个已接受 · 2 轮审查

审查轮次 →

每轮审查后各文件已审查函数中被接受的占比，取自项目历史。每个点是一轮审查；所有图表使用相同刻度，从 0% 到该文件中所有已审查函数。已接受的函数包括审查者确认无需检查的函数，例如内存记账。

当正确的证明仍然是错的

经过检查的证明保证某个陈述能从副本推出，但不保证副本与真实 Python 一致，而测试只覆盖你想到的输入。因此，每个已接受的陈述还会对真实 Python 运行。这抓住了几个有效但仍然错误的证明。

16 TB 的字符串

Python 快速 JSON 编码器的副本假设内存请求总是成功。于是它“证明”了编码器可以为任意嵌套深度构建缩进字符串，包括需要 16 TB 内存的深度。真实 Python 会内存耗尽。修复后的副本现在把每个内存请求都视为可能失败。

九个额外步骤，仅此一次

一份证明称，Python 的 pickle 模块的嵌套调用深度不会超过某个特定数值。这一说法基本属实，但有一个例外：在一个全新的 Python 进程中。在那里，它第一次编码字符串时，会悄悄加载一个文本编解码器，而这次加载又使用了九个额外的嵌套调用。我们的测试从未发现这一点，因为测试框架已经加载了该编解码器。

错误类型有家族关系

在 Python 中，捕获 TypeError 也会捕获任何基于它构建的更具体的错误。有三个独立的副本改为检查错误的确切名称。这三个副本都有证明表明，自定义错误类型可以破坏它们。

内存会回来

Python 的 set 的副本假设，一旦内存被释放，同一地址就永远不会再回来。真实的内存分配器一直在复用地址。CPython 使用“地址是否改变？”的检查来发现用户代码何时替换了集合的内部结构。有了地址复用，这个检查就可能被欺骗。修复该副本后，一个原本被接受的证明变成了一个真实的内存错误，现在已成为我们的一个错误报告。

我们发现了什么

当证明失败是因为 Python 本身有错，而不是副本有错时，我们会将其写成错误报告。每份报告都包含一个简短的脚本，用于在 Python 3.15.2 上展示该错误（大多数也适用于开发版本），还会搜索已报告的重复问题，并诚实评估其重要性。

  • C 与 Python 版本不一致129
  • 其他122
  • 结果错误56
  • 崩溃28
  • 内存损坏27
  • 与文档不符26
  • 错误或消息有误18
  • 缺少输入检查12
按类型划分的 418 份错误报告。“C 与 Python 版本不一致”是指一个模块有两个实现，一个用 C 编写的快速版本和一个 Python 编写的备用版本，它们对同一调用给出不同答案。

大多数问题很小：错误消息有误、某个边缘情况的行为与文档不同、函数的两个版本不一致。大约 55 个问题更严重，仅使用普通 Python 代码就能使 Python 崩溃或损坏其内存，通常是通过让用户代码在 C 代码正在使用容器时更改该容器。Python 不把运行恶意 Python 代码视为安全边界，因此这些是普通错误。尚未出现在 CPython 跟踪器上的问题正在报告给该项目，从这篇文章开始。以下是不同类型的小例子：

崩溃

一个使 Python 崩溃的字典调用

如果同一个类的另一个对象具有该属性而此对象没有，那么用 StrEnum 键对对象的属性字典调用 setdefault 会使解释器崩溃。

class Key(StrEnum):
    NAME = "name"
class User: pass
a = User(); a.name = "ada"
b = User(); b.age = 36
vars(b).setdefault(Key.NAME, "anon")
# Segmentation fault

内存损坏

一个损坏内存的 XML 编辑

对 ElementTree 元素的反向切片赋值应该像列表一样插入。但它却复制了一个子元素而没有获取引用，并丢失了另一个。

e = ET.Element("root")
e[:] = [ET.Element(f"a{i}") for i in range(7)]
e[5:2] = [ET.Element("X")]
[c.tag for c in e]
# 'a2' appears twice, 'a4' is gone

错误有误

一个破坏解析器的电子邮件头

方括号内带空格的 Message-ID 会使 Python 的电子邮件解析器因内部错误而失败。该头来自发送电子邮件的人。

msg = email.message_from_string(
    "Message-ID: <a@[ x]>\n\nhi\n",
    policy=policy.default)
msg["Message-ID"]
# UnboundLocalError

静默错误结果

取决于位置的 Base32 填充

Python 3.15 新增，base32 解码器可以忽略选定的字符。如果 = 是其中之一，它出现的位置仍然会改变结果。

a2b_base32(b"AAAAAAA",  ignorechars=b"=")
# Error: Incorrect padding
a2b_base32(b"AAAA=AAA", ignorechars=b"=")
# b'\x00\x00\x00\x00'

缺少错误

一个消失的枚举错误

给第二个成员赋予枚举值应当报错。如果类的 __repr__ 已损坏，错误会被吞掉，调用就会悄无声息地什么都不做。

class W(Enum):
    A = 1; B = 2
    def __repr__(self): return 5
W.B._add_value_alias_(3)
W.A._add_value_alias_(3)  # returns None

C 和 Python 不一致

两个 pickler，两个上限

Python 有一个 C 实现的 pickler 和一个纯 Python 实现的 pickler。它们在不同的嵌套深度上放弃。这一差异最早于 2008 年被报告，至今仍未解决。

v = []
for _ in range(400): v = [v]
pickle.dumps(v, 5)    # works
pickle._dumps(v, 5)   # RecursionError

每一份报告及其脚本都在仓库里。

为你自己的项目也这样做

这些都不特定于 Python。它适用于任何你有可读源代码、并且能运行一个可用版本的东西：另一种语言、一个库、一种文件格式、一个编译器。对我们来说，起关键作用的是：

  1. 选定一个确切的版本并坚持用它。每一份副本都指向该版本中的具体行。
  2. 先列出全部内容。对照完整清单统计进度，这样就不会有东西被悄悄跳过。
  3. 复制代码，而不是文档。根据文档写出的副本与文档一致，而 bug 恰恰出现在代码与文档不一致的地方。
  4. 让用户代码行为不端。模拟会抛出错误或在操作中途改变状态的回调。最严重的 bug 就出在这里。
  5. 先测试，再证明。对错误的副本做证明是浪费时间。
  6. 当某个命题为假时，保留反例。不要把它弱化到可证明为止。
  7. 用真实实现检验已证明的命题。关于错误副本的有效证明是你能得到的最具误导性的结果。
  8. 只统计独立审查者接受的内容，并让该审查者追问：一个有问题的版本能否通过。

我们的智能体所遵循的指令都在仓库里，且意在复用：给执行工作的智能体用的 AGENTS.md，给审查者用的 REVIEW_PROMPT.md，以及带状态的完整函数清单在 coverage/methods。

相关工作

最接近的项目是 julia-in-lean，它为 Julia 语言做了这件事，并直接启发了本项目1。它在 Lean 中为 Julia 的标准库建模，用 Julia 测试这些模型，记录了约 400 个 bug 并提交了 75 个。它发现 130 个快速证明中有 128 个悄悄把困难情形假设掉了，这一发现塑造了我们的审查规则。最近的一篇论文在 Lean 中为 NVIDIA 的 PTX GPU 指令集建模，以证明 GPU 内核正确2，其基础是早先关于 PTX 内存模型的形式化工作3。

具体到 Python，λπ4 和一个 Python 3.3 的 K framework 语义5 从数学上描述了这门语言；本项目则复制 CPython 的实际代码。JavaScript6,7 和 WebAssembly8 也有类似工作，而 CompCert9 和 seL410 仍是完全验证软件的高标准。在同一输入上比较两个实现——本项目的测试那一半——可以追溯到几十年前11,12。

现状

该项目于 2026 年 10 月 29 日启动。在 26,004 个值得检查的函数中，已有 4,071 个（15.7%）被复制、测试、证明并通过审查。Lean 代码共 613,318 行，分布在 1,539 个文件中，包含 18,898 个定理和引理；其中 3,834 个顶层性质已被证明，588 个被证明为假并给出了反例。Python 的大部分工作仍在前方，尤其是用 Python 本身编写的那大部分标准库。多线程目前不在范围内。在这 57 个文件中，迄今为止复制的每个函数都已通过审查。已接受函数最多的 30 个：

  • Python/bytecodes.c310
  • Grammar/python.gram278
  • Lib/collections/__init__.py184
  • Lib/_pydecimal.py160
  • Lib/_pydatetime.py150
  • Modules/_struct.c122
  • Objects/longobject.c119
  • Objects/listobject.c114
  • Objects/memoryobject.c107
  • Objects/dictobject.c104
  • Objects/bytesobject.c100
  • Objects/exceptions.c97
  • Objects/unicodeobject.c94
  • Objects/bytearrayobject.c93
  • Modules/arraymodule.c84
  • Lib/_collections_abc.py81
  • Modules/_operator.c73
  • Modules/itertoolsmodule.c72
  • Modules/_collectionsmodule.c64
  • Python/codecs.c61
  • Lib/operator.py59
  • Lib/_pyio.py58
  • Objects/typeobject.c57
  • Lib/weakref.py54
  • Objects/genobject.c46
  • Lib/urllib/parse.py46
  • Parser/action_helpers.c43
  • Modules/_zoneinfo.c43
  • Objects/floatobject.c38
  • Objects/tupleobject.c37

该项目是开放的，欢迎提供帮助。CPython 的大部分内容仍未建模：选择一个函数在 coverage/methods 中仍标记为 todo 的文件，按照 AGENTS.md 操作，然后发送拉取请求。对现有工作的独立审查与新模型同样重要。参见 CONTRIBUTING.md。

引用

@misc{andrews2026formalizing,
  author       = {Andrews, David and Zhang, Chao},
  title        = {Formalizing {CPython}: A Lean Model of {CPython} 3.15.2},
  year         = {2026},
  howpublished = {\url{https://broyojo.com/python-formalization/}},
  note         = {Code: \url{https://github.com/Broyojo/python-formalization}}
}

参考文献

  1. M. Cranmer. Formalizing Julia in Lean (and finding 400+ bugs in Base). Julia Discourse, 2026. 代码：MilesCranmer/julia-in-lean。
  2. L. Koska, T. Koska, B. Koska. Formalizing PTX in Lean to Prove GPU Kernel Correctness. arXiv:2611.04447, 2026。
  3. D. Lustig, S. Sahasrabuddhe, O. Giroux. A Formal Analysis of the NVIDIA PTX Memory Consistency Model. ASPLOS 2019。
  4. J. G. Politz, A. Martinez, M. Milano, S. Warren, D. Patterson, J. Li, A. Chitipothu, S. Krishnamurthi. Python: The Full Monty. A Tested Semantics for the Python Programming Language. OOPSLA 2013。
  5. D. Guth. A Formal Semantics of Python 3.3. 硕士论文，伊利诺伊大学厄巴纳-香槟分校，2013。代码：runtimeverification/python-semantics。
  6. M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, G. Smith. A Trusted Mechanised JavaScript Specification. POPL 2014。
  7. D. Park, A. Ştefănescu, G. Roşu. KJS: A Complete Formal Semantics of JavaScript. PLDI 2015。
  8. C. Watt. Mechanising and Verifying the WebAssembly Specification. CPP 2018。
  9. X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM 52(7), 2009。
  10. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, et al. seL4: Formal Verification of an OS Kernel. SOSP 2009。
  11. W. M. McKeeman. Differential Testing for Software. Digital Technical Journal 10(1):100–107, 1998。
  12. X. Yang, Y. Chen, E. Eide, J. Regehr. Finding and Understanding Bugs in C Compilers. PLDI 2011。

来源：Hacker News · broyojo.com

Agent 智能体AI 编码开源生态论文研究#论文/研究#编码#Agent#开源/仓库