プログラミング

CPython の形式化

101 pointsby carnevalem2026年11月10日40 コメント

要約

AIエージェントがCPythonのコードを機械検証可能な言語Leanで1行ずつ書き写し、実Pythonとのテストを経て、418件のバグ報告を発見しました。このプロジェクトは、AIを活用して大規模な既存コードベースの正確性を検証する可能性を示し、多くの潜在的なバグを明らかにしました。

全文翻訳

CPython の形式化

AIエージェントが613,318行のLeanコードを書き、Pythonの内部実装を1行ずつ模倣し、実Pythonに対してあらゆる部分をテストし、コンピュータに全ての証明をチェックさせ、その過程でPythonのバグ報告を418件発見しました。

CPython · Objects/rangeobject.c

static unsigned long get_len_of_range(long lo, long hi, long step) {
    assert(step != 0);
    if (step > 0 && lo < hi)
        return 1UL + (hi - 1UL - lo) / step;
    else if (step < 0 && lo > hi)
        return 1UL + (lo - 1UL - hi) / (0UL - step);
    else
        return 0UL;
}

Lean コピー · RangeSlice/Model.lean

def getLenOfRange (lo hi step : Int) : Int := 
  if step > 0 ∧ lo < hi then
    uadd 1 (usub (usub (toU hi) 1) (toU lo) / toU step)
  else if step < 0 ∧ lo > hi then
    uadd 1 (usub (usub (toU lo) 1) (toU hi)
              / usub 0 (toU step))
  else 0 -- step ≠ 0 は全ての証明で仮定されている
  -- uadd, usub: C の符号なし算術,
  -- 2^64 を超えるとラップアラウンドする

CPython の C ソース (左) からの関数と、エージェントがそれをコピーして書いた Lean (右) の関数。行にカーソルを合わせると、対応する行が表示されます。

TL;DR

Opus 5.5 を CPython、つまりほぼ全ての Python コードを実行するプログラムに向け、その関数を機械検証可能な証明を書くための言語である Lean で書き直させました。
各書き直しは、元のコードを1行ずつコピーし、何かを証明しようとする前に、数万の入力に対して実際の Python と比較してテストされます。
関数は、別のエージェントが作業をチェックし、それが妥当であると同意した場合にのみカウントされます。これまでに 4,071 の関数がそのチェックを通過しました。
結果として、1,539 ファイルにわたる 613,318 行の Lean コードと、18,898 の定理と補題が生成され、これら全てがビルドごとに Lean の証明チェッカーによってチェックされます。
その過程で、証明作業は418件のバグ報告につながりました。ほとんどは軽微ですが、約55件はインタプリタをクラッシュさせたり、通常の Python コードからメモリを破損させたりする可能性があります。

チェック済み・受理済み
書かれたが、まだ受理されていない
未着手

CPython 全体 16%
インタプリタコア 10%
組み込み型 35%
Cモジュール 19%
パーサー 31%
文法規則 100%
標準ライブラリ 9%

CPython 3.15.2 の各部分が、コピー、テスト、証明、レビューによって受理された割合。メモリ管理のような、チェックするものが何もないコードは除外されています。

なぜ手間をかけるのか

Python には厳密な定義がありません。リファレンスマニュアルはありますが、実際には「Python」とは CPython が行うこと全てを指し、CPython は何十万行もの C コードと大規模な標準ライブラリで構成されています。マニュアルは通常の利用法をカバーしています。奇妙なケースについてはほとんど言及しておらず、そこにバグが潜んでいます。例えば、辞書が検索中にその辞書を変更するオブジェクト、アップデートの途中で投げられるエラー、Cコードが想定していた最大値を超えた数値などです。

関数について証明を書くことは、その関数が全てのケースで正確に何をするかを明示的に述べることを強制します。証明チェッカーが受け付けないため、曖昧なままにしておくことはできません。これにより、コードが皆が想定している通りに動作しない場所を見つけるのに役立ちます。

私たちは、CPython のような大規模で古いコードベースでこれがどこまで可能か、そしてほとんどの作業が AI によって行われる場合に結果が信頼性を保つかどうかを見たかったのです。

仕組み

全ての関数は同じ4つのステップを経ます。

コピー
元のコードを1行ずつ、エラーメッセージや奇妙なコーナーケースも含めて、Lean で関数を書き直します。
テスト
コピーと実際の Python を並行して、少なくとも50,000のトリッキーな入力で実行します。不一致があれば、コピーが間違っていることを意味します。
証明
常に真であるべきことを述べ、コンピュータに証明をチェックさせます。もしそれが実際には偽であれば、代わりにそれを証明します。
チェック
作業を行わなかった別のエージェントが、元のコードと比較してレビューし、それを壊そうと試みます。生き残ったものだけがカウントされます。

このページの先頭にあるコードは、CPython の小さな部分、つまり range に含まれる数値の数を計算する C 関数と、その Lean コピーのステップ1です。コピーは、数値が大きくなりすぎてラップアラウンドする際の挙動を含め、C コードの正確な算術演算を維持しています。それについての証明は、この関数、CPython が非常に大きな数に使用する遅いバージョン、そしてそれらを使い分けるコードが、常に同じ正しいカウントを与えることを示しています。

何も証明しない証明

最も困難だったのは、AIエージェントに証明を書かせることではありませんでした。意味のある証明を得ることでした。

最初の試みでは、エージェントに幅広さを求めました。全ての関数をコピーし、それぞれについて少なくとも1つのことを証明するように指示しました。彼らはそれを実行しました。その後、別のレビューで、チェックされた関数の半分未満しか妥当でなく、あるファイルではわずか21%しかありませんでした。証明はすべて正しかったです。ただ、有用なことを何も言っていませんでした。例えば、「この関数が数値を返した場合、その数値は0以上である」というのは真実ですが、常にクラッシュする関数もこれを満たします。

そのため、レビュー担当者は各証明について1つの質問をします。「壊れたバージョンの関数もこれを通過できるか？」

関数のバージョン	「返せば、答えは≥ 0」	「常に正しいカウントを返す」
本物の関数	通過	通過
常にクラッシュ	通過	検出
非常に大きな数に対して0を返す	通過	検出
カウントダウン時に1ずれる	通過	検出

同じ関数に関する2つの真実のステートメント。最初のステートメントは、壊れたバージョンをすべて通過させてしまうため、証明がそれしかない関数はカウントされません。

弱い証明を修正することは、多くの場合、コピーをより現実に近づけるために戻り、例えば、ユーザーコードが関数の途中でエラーを発生させることを許容することを含みます。以下のグラフは、10個のファイルでそれがどのように進んだかを示しています。各点は1回のレビューです。線は時々下がります。レビュー担当者が、受理された証明が実際の Python に関して間違っていると判断した場合、それに依存していた全てが元に戻されます。

受理された関数

100%0%レビュー 1レビュー 5レビュー 1: 142件中0件受理レビュー 2: 142件中2件受理レビュー 3: 142件中41件受理レビュー 4: 142件中130件受理レビュー 5: 142件中135件受理

Objects/typeobject.c 135 of 142 受理 · 5 レビュー

100%0%レビュー 1レビュー 5レビュー 1: 56件中1件受理レビュー 2: 56件中18件受理レビュー 3: 56件中54件受理レビュー 4: 56件中55件受理レビュー 5: 56件中56件受理

Objects/genobject.c 56 of 56 受理 · 5 レビュー

100%0%レビュー 1レビュー 7レビュー 1: 46件中31件受理レビュー 2: 46件中42件受理レビュー 3: 46件中44件受理レビュー 4: 46件中45件受理レビュー 5: 46件中44件受理レビュー 6: 46件中45件受理レビュー 7: 46件中46件受理

Objects/setobject.c 46 of 46 受理 · 7 レビュー

100%0%レビュー 1レビュー 5レビュー 1: 48件中31件受理レビュー 2: 48件中39件受理レビュー 3: 48件中42件受理レビュー 4: 48件中43件受理レビュー 5: 48件中45件受理

Modules/_json.c 45 of 48 受理 · 5 レビュー

100%0%レビュー 1レビュー 9レビュー 1: 39件中21件受理レビュー 2: 39件中30件受理レビュー 3: 39件中35件受理レビュー 4: 39件中34件受理レビュー 5: 39件中33件受理レビュー 6: 39件中34件受理レビュー 7: 39件中29件受理レビュー 8: 39件中36件受理レビュー 9: 39件中37件受理

Lib/enum.py 37 of 39 受理 · 9 レビュー

100%0%レビュー 1レビュー 3レビュー 1: 38件中11件受理レビュー 2: 38件中31件受理レビュー 3: 38件中37件受理

Lib/random.py 37 of 38 受理 · 3 レビュー

100%0%レビュー 1レビュー 2レビュー 1: 43件中9件受理レビュー 2: 43件中41件受理

Objects/abstract.c 41 of 43 受理 · 2 レビュー

100%0%レビュー 1レビュー 2レビュー 1: 33件中19件受理レビュー 2: 33件中33件受理

Objects/rangeobject.c 33 of 33 受理 · 2 レビュー

100%0%レビュー 1レビュー 2レビュー 1: 33件中14件受理レビュー 2: 33件中31件受理

Lib/pickletools.py 31 of 33 受理 · 2 レビュー

100%0%レビュー 1レビュー 2レビュー 1: 40件中29件受理レビュー 2: 40件中35件受理

Modules/binascii.c 35 of 40 受理 · 2 レビュー

レビュー回数 →

各ファイルでレビューされた関数の受理率の推移。各点は1回のレビューを示しており、スケールは全てのグラフで0%からレビューされた全関数まで同じです。受理された関数には、メモリ管理のような、レビュー担当者がチェックするものが何もないことを確認したものが含まれます。

正しい証明が間違っている場合

チェックされた証明は、ステートメントがコピーから導き出されることを保証します。それはコピーが実際の Python と一致することを保証するものではなく、テストは試した入力のみをカバーします。そのため、受理された全てのステートメントは実際の Python と比較して実行されます。これにより、有効でありながら間違っている証明がいくつか発見されました。

16テラバイトの文字列

Python の高速 JSON エンコーダーのコピーは、メモリ要求が常に成功すると仮定していました。そのため、エンコーダーが任意のネスト深度に対してインデント文字列を構築できると「証明」しました。これには16テラバイトのメモリを必要とする深度も含まれます。実際の Python はメモリ不足になります。修正されたコピーは、現在、全てのメモリ要求を失敗する可能性のあるものとして扱います。

9つの追加ステップ、一度だけ

証明によると、Python の pickle モジュールは特定のネスト呼び出し数を超えることはありませんでした。これはブランドニューな Python プロセスを除いて真実であることが判明しました。その場合、文字列をエンコードする最初の時に、テキストコーデックを静かにロードし、そのロードは9つの追加のネスト呼び出しを使用します。テストハーネスが既にコーデックをロードしていたため、私たちのテストはそれを決して見ませんでした。

エラータイプにはファミリーがある

Python では、TypeError をキャッチすると、それを基にしたより具体的なエラーもキャッチします。3つの別々のコピーが、エラーの正確な名前を代わりにチェックしました。これら3つすべてで、カスタムエラータイプが壊れるという証明がありました。

戻ってくるメモリ

Python の set のコピーは、メモリが解放されたら、同じアドレスが二度と戻ってこないと仮定していました。実際のメモリ割り当て器は、アドレスを頻繁に再利用します。CPython は、「アドレスが変更されたか？」というチェックを使用して、ユーザーコードがセットの内部をスワップアウトしたかどうかを検出します。再利用により、そのチェックは誤解される可能性があります。コピーの修正は、受理された証明を実際のメモリバグに変えました。これは現在、私たちのバグ報告の1つです。

見つかったこと

証明が Python 自体の間違いで失敗した場合、コピーの間違いではない場合、それをバグ報告として記録します。各報告には、Python 3.15.2 (ほとんどの場合、開発バージョンでも) でバグを示す短いスクリプト、重複報告の検索、そしてその重要度に関する正直な評価が含まれます。

C と Python のバージョン間の不一致 129
その他 122
間違った結果 56
クラッシュ 28
メモリ破損 27
ドキュメントと一致しない 26
間違ったエラーまたはメッセージ 18
入力チェック不足 12

タイプ別の418件のバグ報告。「CとPythonのバージョン間の不一致」とは、モジュールに2つの実装（Cでの高速なものとPythonでのバックアップ）があり、同じ呼び出しに対して異なる答えを出すことを意味します。ほとんどは軽微です。エラーメッセージの間違い、ドキュメントと異なるエッジケースの動作、関数の2つのバージョンの不一致などです。約55件はより深刻で、通常の Python コードのみを使用して Python をクラッシュさせたり、メモリを破損させたりする可能性があります。これは通常、ユーザーコードが C コードが使用中のコンテナを変更することによって発生します。Python は悪意のある Python コードの実行をセキュリティ境界として扱わないため、これらは通常のバグです。CPython のトラッカーにまだ載っていないものは、この投稿から始まり、プロジェクトに報告されています。種類の異なる6つの小さな例を以下に示します。

クラッシュ

Python をクラッシュさせる辞書呼び出し

オブジェクトの属性辞書に対して StrEnum キーで setdefault を呼び出すと、同じクラスの別のオブジェクトがその属性を持ち、現在のオブジェクトが持っていない場合にインタプリタがクラッシュします。

class Key(StrEnum):
    NAME = "name"
class User: pass
a = User(); a.name = "ada"
b = User(); b.age = 36
vars(b).setdefault(Key.NAME, "anon")
# Segmentation fault

メモリ破損

メモリを破損させる XML 編集

ElementTree 要素の逆スライスへの代入は、リストの場合と同様に挿入されるはずです。代わりに、参照を取らずに子を1つ複製し、もう1つを失います。

e = ET.Element("root")
e[:] = [ET.Element(f"a{i}") for i in range(7)]
e[5:2] = [ET.Element("X")]
[c.tag for c in e]
# 'a2' が2回現れ、'a4' が失われる

間違ったエラー

パーサーを壊すメールヘッダー

角括弧の中にスペースがある Message-ID は、Python のメールパーサーを内部エラーで失敗させます。ヘッダーはメールを送信した人から来ます。

msg = email.message_from_string(
    "Message-ID: <a@[ x]>\n\nhi\n",
    policy=policy.default)
msg["Message-ID"]
# UnboundLocalError

静かに間違った結果

位置に依存する Base32 パディング

Python 3.15 で新しく追加された base32 デコーダーは、選択した文字を無視できます。= がその中の1つである場合、それが現れる位置によって結果が変わります。

a2b_base32(b"AAAAAAA",  ignorechars=b"=")
# Error: Incorrect padding
a2b_base32(b"AAAA=AAA", ignorechars=b"=")
# b'\x00\x00\x00\x00'

エラーの欠落

消える enum エラー

enum 値を2番目のメンバーに与えるとエラーが発生するはずです。クラスの __repr__ が壊れている場合、エラーは飲み込まれ、呼び出しは静かに何も行いません。

class W(Enum):
    A = 1; B = 2
    def __repr__(self): return 5
W.B._add_value_alias_(3)
W.A._add_value_alias_(3)  # None を返す

C と Python の不一致

2つのピクラー、2つの制限

Python には C ピクラーと純粋な Python ピクラーがあります。それらは異なるネスト深度で停止します。この違いは2008年に初めて報告され、まだ未解決です。

v = []
for _ in range(400): v = [v]
pickle.dumps(v, 5)    # 動作する
pickle._dumps(v, 5)   # RecursionError

スクリプト付きの各レポートは、リポジトリにあります。

あなた自身のプロジェクトでこれを実行する

これらは Python に固有のものではありません。ソースコードを読み、実行可能なバージョンがあるものであれば、何にでも適用できます。別の言語、ライブラリ、ファイル形式、コンパイラなどです。私たちにとって違いを生んだのは次の点です。

正確な1つのバージョンを選択し、それに固執してください。全てのコピーはそのバージョンの特定の行を指します。
まず全てをリストアップしてください。進捗を完全なリストに対してカウントし、何も静かにスキップされないようにします。
ドキュメントではなくコードをコピーしてください。ドキュメントから書かれたコピーはドキュメントと一致し、バグはコードとドキュメントが一致しない場所にあります。
ユーザーコードを誤動作させることを許容してください。エラーを発生させたり、操作の途中で変更したりするコールバックをモデル化してください。そこに最悪のバグがありました。
証明する前にテストしてください。間違ったコピーについて証明をすることは時間の無駄です。
何かが偽の場合、反例を保持してください。証明可能になるまでステートメントを弱めないでください。
証明されたステートメントを実際のコードと比較してチェックしてください。間違ったコピーに関する有効な証明は、得られる最も誤解を招く結果です。
独立したレビュー担当者が受理したものだけをカウントし、そのレビュー担当者に壊れたバージョンが通過できるかどうかを尋ねてください。

私たちのエージェントが作業した指示はリポジトリにあり、再利用可能です。エージェントの作業を行うエージェント用の AGENTS.md、レビュー担当者用の REVIEW_PROMPT.md、そしてステータス付きの関数の完全なリストは coverage/methods にあります。

現在の状況

プロジェクトは2026年10月29日に開始されました。チェックする価値のある26,004関数のうち4,071件 (15.7%) がコピー、テスト、証明、レビューを経て受理されています。Lean コードは1,539ファイルに613,318行あり、18,898の定理と補題を含んでいます。トップレベルのプロパティのうち3,834件が証明され、588件は反例とともに偽であることが証明されています。Python の大部分、特に Python 自体で書かれた標準ライブラリの大きな部分はまだ未着手です。マルチスレッドは現在スコープ外です。これら57ファイルでは、これまでにコピーされた全ての関数がレビューを通過しました。受理された関数が最も多い30ファイルは次のとおりです。

Python/bytecodes.c 310
Grammar/python.gram 278
Lib/collections/__init__.py 184
Lib/_pydecimal.py 160
Lib/_pydatetime.py 150
Modules/_struct.c 122
Objects/longobject.c 119
Objects/listobject.c 114
Objects/memoryobject.c 107
Objects/dictobject.c 104
Objects/bytesobject.c 100
Objects/exceptions.c 97
Objects/unicodeobject.c 94
Objects/bytearrayobject.c 93
Modules/arraymodule.c 84
Lib/_collections_abc.py 81
Modules/_operator.c 73
Modules/itertoolsmodule.c 72
Modules/_collectionsmodule.c 64
Python/codecs.c 61
Lib/operator.py 59
Lib/_pyio.py 58
Objects/typeobject.c 57
Lib/weakref.py 54
Objects/genobject.c 46
Lib/urllib/parse.py 46
Parser/action_helpers.c 43
Modules/_zoneinfo.c 43
Objects/floatobject.c 38
Objects/tupleobject.c 37

プロジェクトは公開されており、協力者を歓迎します。CPython の大部分はまだモデル化されていません。coverage/methods で todo とマークされているファイルを選択し、AGENTS.md に従い、プルリクエストを送信してください。既存の作業の独立したレビューも、新しいモデルと同じくらい重要です。CONTRIBUTING.md を参照してください。

引用

@misc{andrews2026formalizing,
  author       = {Andrews, David and Zhang, Chao},
  title        = {Formalizing {CPython}: A Lean Model of {CPython} 3.15.2},
  year         = {2026},
  howpublished = {\url{https://broyojo.com/python-formalization/}},
  note         = {Code: \url{https://github.com/Broyojo/python-formalization}}
}

参考文献

M. Cranmer. Formalizing Julia in Lean (and finding 400+ bugs in Base). Julia Discourse, 2026. Code: MilesCranmer/julia-in-lean.
L. Koska, T. Koska, B. Koska. Formalizing PTX in Lean to Prove GPU Kernel Correctness. arXiv:2611.04447, 2026.
D. Lustig, S. Sahasrabuddhe, O. Giroux. A Formal Analysis of the NVIDIA PTX Memory Consistency Model. ASPLOS 2019.
J. G. Politz, A. Martinez, M. Milano, S. Warren, D. Patterson, J. Li, A. Chitipothu, S. Krishnamurthi. Python: The Full Monty. A Tested Semantics for the Python Programming Language. OOPSLA 2013.
D. Guth. A Formal Semantics of Python 3.3. M.S. thesis, University of Illinois at Urbana-Champaign, 2013. Code: runtimeverification/python-semantics.
M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, G. Smith. A Trusted Mechanised JavaScript Specification. POPL 2014.
D. Park, A. Ştefănescu, G. Roşu. KJS: A Complete Formal Semantics of JavaScript. PLDI 2015.
C. Watt. Mechanising and Verifying the WebAssembly Specification. CPP 2018.
X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM 52(7), 2009.
G. Klein, K. Elphinstone, G. Heiser, J. Andronick, et al. seL4: Formal Verification of an OS Kernel. SOSP 2009.
W. M. McKeeman. Differential Testing for Software. Digital Technical Journal 10(1):100–107, 1998.
X. Yang, Y. Chen, E. Eide, J. Regehr. Finding and Understanding Bugs in C Compilers. PLDI 2011.

CPython の形式化

要約

全文翻訳

CPython の形式化

TL;DR

なぜ手間をかけるのか

仕組み

何も証明しない証明

正しい証明が間違っている場合

16テラバイトの文字列

9つの追加ステップ、一度だけ

エラータイプにはファミリーがある

戻ってくるメモリ

見つかったこと

Python をクラッシュさせる辞書呼び出し

メモリを破損させる XML 編集

パーサーを壊すメールヘッダー

位置に依存する Base32 パディング

消える enum エラー

2つのピクラー、2つの制限

あなた自身のプロジェクトでこれを実行する

関連研究

現在の状況

引用

参考文献