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

Formalizing CPython

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

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