Today for AI
返回全部资讯
AI 智能体用 Lean 形式化 CPython 并发现 418 个缺陷Hacker News AIT2·基座大模型

AI 智能体用 Lean 形式化 CPython 并发现 418 个缺陷

原标题：Formalizing CPython
78AI 研判分

研究团队用 Opus 5.5 智能体将 CPython 3.15.2 的内部实现逐行翻译为 61.3 万行 Lean 代码，并对照真实 Python 逐项测试、由机器校验全部证明，过程中向 CPython 提交了 418 条缺陷报告。该工作首次给出可机器验证的 CPython 形式化模型，为解释器语义正确性提供了新的工程范式。

关联知识实体

工具CPython术语差分测试术语形式化验证工具Lean模型Opus 5.5

报道正文

本文目录20 个章节

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

CPython · Objects/rangeobject.c

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

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 源码中的一个函数，右侧是 agent 为其编写的 Lean 复刻版。将鼠标悬停在某一行上即可查看其对应行。

摘要

  • 我们让 Opus 5.5 面向 CPython——运行几乎所有 Python 代码的程序——用 Lean 重写其函数，Lean 是一种用于编写机器可检验证明的语言。
  • 每个重写版本都逐行复刻原始实现，并在任何人尝试对其证明任何性质之前，先针对真实 Python 在数万个输入上进行测试。
  • 一个函数只有在第二个未参与编写的 agent 检查工作并认可其成立后，才算通过。目前已有 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 代码加上一个庞大的标准库。手册涵盖的是正常用法，对边缘情况几乎只字不提，而 bug 恰恰藏在那里：一个对象在字典查找它的过程中修改了该字典，一次更新进行到一半时抛出的错误，一个比 C 代码当初设计所能处理的最大值还大 1 的数字。

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

我们想看看，在一个像 CPython 这样庞大而古老的代码库上，这件事能做到什么程度，以及当大部分工作由 AI 完成时，结果是否仍然可信。

工作原理

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

  1. 复制 用 Lean 重写该函数，逐行遵循原始代码，包括其错误消息和古怪的边角情况。
  2. 测试 在至少 50,000 个刁钻输入上并排运行副本和真正的 Python。任何不一致都意味着副本有误。
  3. 证明 陈述某个应当始终成立的性质，让计算机检查证明。如果它实际上是假的，那就改为证明这一点。
  4. 核查 由一个没有参与工作的第二个 agent 对照原始代码进行审查，并尝试攻破它。只有经受住考验的才算数。

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

什么也证明不了的证明

最难的部分不是让 AI agent 写出证明，而是得到真正有意义的证明。

我们最初的尝试是要求智能体追求广度：复制每一个函数，并至少证明每个函数的一件事。它们做到了。随后一项单独的审查发现，它检查的函数中只有不到一半经得起推敲，而在一个文件里这一比例仅为 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 使用“地址是否改变？”的检查来发现用户代码何时替换了 set 的内部结构。在地址复用的情况下，这个检查可能被欺骗。修复这份副本后，一个原本被接受的证明变成了一个真实的内存 bug，如今已成为我们的 bug 报告之一。

我们的发现

当一项证明失败的原因在于 Python 本身有错、而非副本有错时，我们会将其写成 bug 报告。每份报告都包含一个简短的脚本，用于在 Python 3.15.2 上展示该 bug（大多数也能在开发版上复现），还会检索是否已有重复报告，并如实评估其影响程度。

  • C 与 Python 版本不一致129
  • 其他122
  • 结果错误56
  • 崩溃28
  • 内存损坏27
  • 与文档不符26
  • 错误或消息有误18
  • 缺少输入检查12

按类型划分的 418 份 bug 报告。“C 与 Python 版本不一致”是指某个模块有两套实现，一套是 C 编写的快速版本，另一套是 Python 编写的备用版本，而它们对同一调用给出不同结果。

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

崩溃

一个导致 Python 崩溃的字典调用

对对象的属性字典使用 StrEnum 键调用 setdefault 时，如果同一类的另一个对象拥有该属性而当前对象没有，解释器就会崩溃。

PYTHON
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 元素的反向切片赋值本应像列表一样执行插入操作。但它却复制了一个子元素却没有增加引用，同时丢失了另一个子元素。

PYTHON
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 的邮件解析器因内部错误而失败。该邮件头来自发送邮件的人。

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 解码器可以忽略指定的字符。如果 = 是其中之一，它出现的位置仍然会改变结果。

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

缺失的错误

一个消失的枚举错误

将枚举值赋给第二个成员本应引发错误。如果该类的 __repr__ 有问题，错误会被吞掉，调用会静默地什么都不做。

PYTHON
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 年被报告，至今仍未解决。

PYTHON
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. 只统计独立评审者认可的内容， 并让该评审者追问：一个有缺陷的版本是否也能通过？

我们的 agent 所遵循的指令都在仓库中，且意在可复用：AGENTS.md 供执行工作的 agent 使用，REVIEW_PROMPT.md 供评审者使用，而包含各函数及其状态的完整清单在 coverage/methods。

相关工作

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

具体到 Python，λπ4 以及 Python 3.3 的 K 框架语义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，并提交 pull request。对现有工作的独立审查与新模型同等重要。参见 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}}
}