AI 智能体已将 CPython 解释器的核心逻辑逐行复刻为 Lean 代码，总计生成 613,318 行。在真实 Python 环境中经过海量输入测试及自动化证明检查后，该项目共发现 418 个漏洞报告，其中约 55 个可能导致解释器崩溃或内存破坏。
核心进展与数据
该项目利用 Opus 5.5 智能体，将 CPython 函数重写为可用于机器可检查证明的 Lean 语言。关键成果包括：
- 代码规模：涵盖 1,539 个文件，包含 613,318 行 Lean 代码、18,898 个定理和引理。
- 验证状态：4,071 个函数已通过独立智能体审查，确保证明成立且与真实 Python 行为一致。
- 漏洞发现：在证明过程中识别出 418 个漏洞。大多数为边缘情况或小问题，但部分严重漏洞可通过普通 Python 代码触发内存破坏或崩溃。
为何进行形式化验证
Python 缺乏精确的书面定义，实际行为依赖于 CPython 这一数十万行 C 代码构成的解释器。官方手册往往忽略异常情况，而这正是漏洞的高发区，如字典搜索期间修改对象、数值溢出等。
编写形式化证明迫使开发者明确函数在所有情况下的确切行为，消除模糊空间。本项目旨在探索在 CPython 这样庞大且古老的代码库中，由 AI 主导的形式化验证能否产出值得信赖的结果。
工作原理与审查机制
每个函数的处理遵循四个步骤：复制 C 代码逻辑至 Lean、针对数万种输入与真实 Python 进行测试、生成形式化证明、由未参与编写的智能体进行独立审查。
审查的核心标准是：一个损坏的函数版本能否也能通过这个证明？早期尝试因证明过于宽泛（如仅证明返回值非负）而被否决。修复薄弱证明需使 Lean 副本更贴近现实，例如允许中途抛出错误或处理内存分配失败。
此外，每个接受的陈述都会在真实 Python 上运行，以捕捉那些形式上正确但与实际情况不符的“错误证明”。例如，JSON 编码器曾假设内存请求总是成功，导致证明出可构建 16 TB 字符串的荒谬结论；修复后将内存请求视为可能失败的操作，从而揭示了潜在问题。
典型漏洞案例
发现的漏洞涵盖多种类型，以下是六个代表性示例：
- 崩溃：在特定条件下对对象属性字典使用
StrEnum键调用setdefault会导致解释器段错误。 - 内存破坏：ElementTree 元素的反向切片赋值未正确处理引用，导致子节点重复或丢失。
- 解析错误：带有空格的 Message-ID 会导致邮件解析器抛出
UnboundLocalError。 - 静默错误：Base32 解码器在忽略特定字符时，填充符
=的位置会影响结果，导致不一致行为。 - 错误吞没：若枚举类的
__repr__损坏，添加值别名时的错误会被静默忽略。 - 实现不一致：C pickler 和纯 Python pickler 在处理嵌套深度限制时存在差异，该问题自 2008 年起未被解决。
项目现状与贡献
项目始于 2026 年 10 月 29 日，针对 Python 3.15.2 版本。在 26,004 个待检查函数中，已有 15.7%（4,071 个）完成复制、测试、证明并通过审查。目前，多线程支持尚未纳入范围，标准库中由 Python 编写的部分仍有大量工作待完成。
该项目开源并欢迎社区贡献。开发者可依据仓库中的 AGENTS.md 和 REVIEW_PROMPT.md 指令，选择标记为 todo 的文件进行建模或参与独立审查。相关工作受 julia-in-lean 项目启发，后者曾在 Julia 语言中发现类似数量的漏洞。