# CPython 形式化研究：AI 智能体用 Lean 建模，整理出 418 份缺陷报告

> 原标题：Formalizing CPython

- 来源：Hacker News 首页
- 发布时间：2026-11-10T01:56:48.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/k5plpobz1hquce4frqem93plo
- 原文：https://broyojo.com/python-formalization/

## 摘要

CPython 形式化项目使用 Opus 5.5 将 CPython 3.15.2 的函数逐行改写为 Lean，已有 4,071 个函数通过测试、形式化验证与独立智能体审查，占待检查函数的 15.7%。

## 推荐理由

CPython 形式化项目将逐行建模、差分测试与独立审查结合，用真实运行结果检验形式化结论是否遗漏异常与内存行为。

## 锐评

能挖出 418 个缺陷报告，里头还有 55 个能让解释器崩溃或破坏内存，这个产出我觉得很有分量。

CPython 跑了这么多年，才被改写了 15.7% 的函数就暴露出这么多深坑。Lean 的形式化验证有机器检查器兜底，通不过就是通不过，完全不给大模型胡说八道的空间。把算力花在 Opus 5.5 逐行重写和双 agent 审查上，能抓出 55 个能弄崩系统的实锤 bug，这笔账算得很值。