一名开发者让 Claude Opus 5.5 用 Lean 对 CPython 进行形式化，写出 613,318 行代码

开发者 broyojo42 表示，他们让 Claude Opus 5.5 用 Lean 对 CPython 进行形式化：共 613,318 行代码，逐行复刻 Python 的内部实现，并与真实解释器进行测试、由 Lean 验证。他们称，在这一过程中，模型还发现了 Python 中的真实漏洞，包括可由普通 Python 代码触发的崩溃。

这篇帖子是作者本人的说法；截至 11 月 10 日，该帖在 X 上获得了 2,066 点赞。Astral 的 Charlie Marsh 转发了这篇帖子。