Hai nhà nghiên cứu ở Georgia Tech đã dùng AI để viết lại CPython 3.15.2 bằng ngôn ngữ kiểm chứng Lean. Chỉ trong 11 ngày, họ tìm ra 418 lỗi có thể tái hiện, trong đó khoảng 55 lỗi đủ nghiêm trọng để làm sập trình thông dịch. Lỗi nổi bật nhất chỉ cần 5 dòng Python với dict.setdefault là đủ gây segfault, và bản sửa đã được phê duyệt.

Đây là lần đầu AI kiểm chứng chính thức tìm ra lỗi thật trong CPython.

5 dòng code làm sập Python 3.15

Đoạn code gây lỗi không cần thread hay extension C:

from enum import StrEnum
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

Nguyên nhân: các object cùng class chia sẻ một bảng tên thuộc tính chung. Khi gọi setdefault trên __dict__ của một instance, code xử lý bỏ qua trường hợp tên đã có trong bảng chung nhưng chưa có trên object này, rồi dereference một con trỏ null. Lỗi đã được báo cáo là issue gh-161693; bản sửa PR 161704 đã được core developer Inada Naoki phê duyệt.

AI đã làm điều đó như thế nào?

David Andrews, nghiên cứu sinh tiến sĩ tại Georgia Tech (hướng dẫn bởi Chao Zhang), bắt đầu dự án ngày 29/10/2026. Claude Opus 5.5 viết một mô hình Lean 4 của CPython 3.15.2, bám sát source C và Python. Mỗi hàm được viết lại bằng Lean, chạy đối chiếu với trình thông dịch thật trên 50.000 input, rồi thử chứng minh đúng với mọi input — thất bại để lại counterexample, chính là input gây lỗi. Một agent thứ hai rà soát lại, kiểm tra xem bản cài đặt hỏng có vượt qua được chứng minh không.

Kết quả: 613.318 dòng Lean, 18.898 định lý, 4.071 trên 26.004 hàm đã qua rà soát (15,7%), chi phí khoảng 6.978 USD.

6 lỗi đã được báo cáo chính thức

Ngày 9/11/2026, nhóm nghiên cứu nộp 6 lỗi crash lên CPython, tất cả do chính Andrews đọc và tái hiện bằng tay; tính đến ngày 10/11 cả 6 vẫn đang mở:

  • gh-161693: dict.setdefault gây segfault — bản sửa PR 161704 đã được phê duyệt.
  • gh-161692: functools.partial tràn bộ đệm stack (mới ở 3.15).
  • gh-161690: dict.fromkeys() gắn cờ GC sai (mới ở 3.15).
  • gh-161688: bytearray.strip() gây use-after-free.
  • gh-161689: gán slice ngược trên ElementTree hỏng bộ nhớ.
  • gh-161691: memoryview vẫn bị dùng sau khi đã release.

Cần tỉnh táo: đây chưa phải “Python đã được chứng minh đúng”

Chứng minh chỉ đúng với bản sao Lean, không đảm bảo bản sao khớp hoàn toàn với CPython thật. Hơn một nửa số chứng minh ban đầu đã bị loại vì đúng về mặt hình thức nhưng vô nghĩa. Ngoài ra, 418 báo cáo chưa phải 418 bug đã xác nhận; chỉ 6 lỗi được nộp chính thức, và các lỗi này chỉ là bug thường, không phải lỗ hổng bảo mật.

Điều này có ý nghĩa gì với bạn

Nếu bạn chạy Python 3.15.2, lỗi setdefault chỉ kích hoạt khi StrEnum làm key với instance dict dạng split-table — hiếm gặp, nhưng hãy cập nhật bản vá 3.15.x tiếp theo ngay khi có.

Bài viết liên quan

Câu hỏi thường gặp

Lỗi setdefault có ảnh hưởng tới code Python thông thường không?

Hiếm khi — chỉ khi StrEnum làm key cho setdefault trên __dict__ của instance có tên thuộc tính trong bảng tên chung của class.

418 báo cáo có nghĩa là Python 3.15 có 418 bug?

Không. Đó là 418 trường hợp tái hiện được, chưa phải bug đã xác nhận. Chỉ 6 lỗi crash được nộp chính thức.

Khi nào có bản vá cho lỗi setdefault?

Bản sửa PR 161704 đã được phê duyệt và đang chờ merge, đồng thời được gắn nhãn backport về Python 3.15 và 3.14.

💬 Tin này ảnh hưởng tới dự án của bạn thế nào? Chia sẻ góc nhìn của bạn trong phần bình luận — mình đọc hết và sẽ tổng hợp những ý hay nhất.

Nguồn tham khảo