一名開發者讓 Claude Opus 5.5 用 Lean 將 CPython 形式化，產出 613,318 行程式碼

開發者 broyojo42 表示，他們讓 Claude Opus 5.5 用 Lean 撰寫 CPython 的形式化版本：共 613,318 行，逐行複製 Python 的內部實作，並以實際直譯器進行測試，再交由 Lean 檢查。他們表示，模型在過程中還發現了 Python 的真實 bug，包括能由一般 Python 程式碼觸發的當機問題。

這篇貼文是作者本人的說法；截至 11 月 10 日，該貼文在 X 上獲得 2,066 點。Astral 的 Charlie Marsh 也分享了這篇貼文。