Claude Chứng Minh 123 Thư Viện Không Sập: Hãng Nói 239 Điểm Vào, Kho Công Khai Mới Có 60
Ngày 22/10/2026 Anthropic và Theorem nói Claude viết chứng minh hình thức cho 239 điểm vào của 123 thư viện OSS-Fuzz: mọi đầu vào dưới 64 MB không làm bản RISC-V sập, kèm "hàng trăm" lỗi tìm được. Locaith mở kho công khai ngày 25/10: bản đầu tiên chứng minh 60 điểm vào của 25 dự án (138 trong 20.164
Ngày 22/10/2026, Nhóm Frontier Red Team của Anthropic và công ty Theorem công bố rằng Claude đã viết chứng minh hình thức cho 239 điểm vào (entry point) của 123 thư viện mã nguồn mở trong OSS-Fuzz: với mọi đầu vào dưới 64 MB, chương trình đã biên dịch sẽ không sập hay chạm lỗi bộ nhớ, trong những giả định hẹp nêu rõ. Cùng ngày Theorem đăng một kho công khai để ai cũng kiểm lại được. Locaith mở kho đó ngày 25/10: bản phát hành đầu tiên có chứng minh cho 60 điểm vào của 25 dự án, và mô tả phát biểu được chứng minh hẹp hơn câu "luôn thoát bình thường" trong bài của hãng.
Hãng nói gì đã được chứng minh
Fuzzing ném rất nhiều đầu vào ngẫu nhiên vào một điểm vào để tìm lần sập, nhưng không bao giờ phủ hết mọi đường chạy. Cách của Anthropic và Theorem: lấy bài fuzz có sẵn của dự án, biến nó thành một đặc tả "bài này không bao giờ sập với mọi đầu vào dưới 64 MB", trên chính các lệnh máy RISC-V của bản đã biên dịch, rồi để Claude viết chứng minh. Bộ kiểm chứng Rocq kiểm chứng minh theo đặc tả, nên theo bài, gần như không cần người đọc 180 triệu dòng Rocq mà Claude viết (mỗi chứng minh điển hình khoảng 600.000 dòng cho tệp nhị phân trung vị 18.000 lệnh). Thứ phải tin chỉ gồm mô hình hình thức của RISC-V và tiến trình Linux, nội dung đúng của các định lý, và chính bộ kiểm Rocq.
Hãng nêu rõ các giả định: chương trình chạy như tệp tĩnh đơn luồng, ngân sách bộ nhớ cố định, trên CPU RISC-V với Linux, liên kết musl. Phần lớn người dùng chạy các thư viện này trên x86 hoặc ARM và liên kết động với glibc, nên hãng viết rằng "đã kiểm chứng hình thức" không có nghĩa "không có lỗi". Hãng cũng nói ASan không bắt hết lỗi bộ nhớ, không phải mọi điểm vào của mỗi thư viện đều được chứng minh, và chương trình gọi thư viện có thể dùng sai.
Lỗi tìm được trong lúc chứng minh
Trong lúc cố chứng minh, Claude tìm ra "hàng trăm" lỗi (hãng không đưa số chính xác) và tự vá để chứng minh tiếp. Hãng nêu ví dụ không gọi tên thư viện: một lỗi tràn ngược bộ đếm trong bản sao của một bộ giải nén dẫn tới ghi ngoài vùng nhớ, chỉ khi đầu vào cỡ 20 MB và có một bố cục hiếm; một lỗi đọc ngoài vùng ở bộ giải mã ảnh cần đầu vào 64 MB và hơn 2 GB bộ nhớ; một lỗi cần chuỗi lệnh gọi qua hai tay cầm tới cùng một tệp; và việc tìm lại CVE-2026-56132 của libexpat, cần đầu vào lồng sâu. Một lỗi logic không gây sập: tính năng giới hạn tệp mà ứng dụng được nạp không phải lúc nào cũng được áp dụng. Locaith tra bản ghi CVE gốc: CVE-2026-56132 công bố ngày 19/6/2026, ảnh hưởng libexpat trước 2.8.2, là lỗi tràn bộ nhớ heap trong doProlog do cấp phát lại mảng "scaffold" sai khi chia sẻ cấu trúc dữ liệu giữa các parser. Bản ghi CVE không nhắc "đầu vào lồng sâu"; Locaith không đủ thông tin để nói hai mô tả có khớp không.
Việc để mô hình tự vá có nguy cơ gian lận phần thưởng (sửa chương trình thành bản tầm thường không bao giờ sập để chứng minh dễ hơn). Hãng nói đã phạt mỗi bản vá, thưởng thêm khi chứng minh được bản vá chỉ đổi ít đầu vào nào, và ghi nhật ký rồi kiểm các bản vá. Hãng không nêu bao nhiêu bản vá, trên thư viện nào, nên chứng minh nào áp dụng cho mã đã vá và mã gốc là điều người ngoài chưa đếm được.
Locaith mở kho công khai: 60 điểm vào, 25 dự án
Kho theorem-labs/oss-verify-proofs (giấy phép MIT) được tạo lúc 17:20 UTC ngày 22/10/2026; Locaith đọc README, nhật ký thay đổi và tài liệu nguồn gốc ngày 25/10, nhưng không chạy bộ kiểm lại chứng minh nào. Theo README và CHANGELOG của bản 2026.10.0, bản phát hành đầu tiên có 20.164 phát biểu về 2.148 harness của 427 dự án OSS-Fuzz mà Theorem biên dịch được; trong đó 138 phát biểu đã chứng minh (60 điểm vào, 25 dự án), 229 bị mô hình chặn, 19.797 còn mở. Các chứng minh được "chuyển" từ chứng minh Anthropic cấp phép (Apache-2.0 hoặc MIT) sang tệp nhị phân và phiên bản mô hình của bản này; người viết là các tác tử mô hình ngôn ngữ, còn công nhận một chứng minh là nhờ nhân Rocq 9.2.0 kiểm.
| Bài của Anthropic (22/10) | Kho công khai (Locaith đọc 25/10) | |
|---|---|---|
| Quy mô | 239 điểm vào, 123 thư viện OSS-Fuzz | 60 điểm vào, 25 dự án (khoảng 25% số điểm vào và 20% số thư viện nếu so thẳng) |
| Phát biểu được chứng minh | "luôn thoát bình thường", không lỗi bộ nhớ hay assertion hỏng, mọi đầu vào dưới 64 MB | Phát biểu "đồng thuận": bản có sanitizer và bản thường có cùng hành vi quan sát được và không chạm lỗi, trên mọi đầu vào mà bản thường nằm trong ngân sách bộ nhớ (2 GiB với ASan). README nói rõ không loại trừ trường hợp chạy mãi không dừng, và bản này chưa có phát biểu "dừng" nào được chứng minh |
| Phần còn lại | Hãng chỉ phát hành một phần: chứng minh của các bài fuzz không cần vá và đặc tả của bài chưa chứng minh được; không phát hành chứng minh có thể lộ lỗi chưa vá | 19.797 phát biểu còn mở trên 20.164; mô hình hình thức của Linux (LPS) nói rõ là "best effort", "không đầy đủ", có giả định không tự kiểm |
Hai chỗ lệch cần đọc kỹ. Thứ nhất, con số 239 và 123 chỉ hãng công bố; người ngoài chỉ kiểm được phần nằm trong kho, và các chứng minh trong kho đã được chuyển sang tệp nhị phân và phiên bản mô hình của bản này, nên chưa chắc là đúng những tệp mà hãng đếm. Thứ hai, câu "luôn thoát bình thường" trong bài nghe như bao gồm cả việc chương trình kết thúc, trong khi kho công khai nói rõ các chứng minh của bản này không bao gồm việc dừng. Locaith không biết các chứng minh chưa công bố có phát biểu mạnh hơn không; đây là hai cách diễn đạt khác nhau, chưa phải bằng chứng hãng nói sai.
Chi phí: càng ngày càng ít token, nhưng chưa có giá
Bài nói chứng minh có thể cần hàng trăm triệu token và không nêu chi phí bằng tiền. Hãng dựng 36 nhiệm vụ nhỏ từ mã OSS-Fuzz: Opus 5.5 chứng minh một nửa số đó bằng khoảng 40% ít token hơn Opus 5 (mỗi nhiệm vụ ba lần thử một tác tử, ngân sách 5 triệu token, tính là xong khi lần thử đầu hoàn thành). Khi cho các tác tử dùng chung không gian làm việc và sao chép chứng minh của nhau, cần ít hơn 17% token; trong 34 chứng minh hoàn thành, tác tử làm một mình tốn nhiều hơn ở 30 chứng minh, và hai chứng minh làm một mình không hoàn thành.
Còn lại: kết quả phụ và lời của hãng chưa kiểm được
- zlib trong nhân Linux. Claude viết đặc tả RFC 1950 rồi chứng minh bản cài đặt zlib của nhân khớp, ở mức tệp nhị phân x86 với mô hình x86 do Claude tạo và kiểm; hãng nói tìm được vài lỗi nhỏ không khai thác được ở trường hợp biên và đang gửi lên thượng nguồn. Hãng nói đã làm tương tự cho khoảng nửa tá thư viện khác, không nêu tên.
- Trình thông dịch Python viết bằng Rust. Claude viết và chứng minh bằng Verus rằng nó bám ngữ nghĩa CPython trong một bài báo; chạy 1,7 triệu chương trình Python sinh ngẫu nhiên, hành vi giống CPython ở 99,95% bài thử. Đây là phép đo thực nghiệm chứ không phải chứng minh về 1,7 triệu chương trình.
- Trình đọc PDF. Hãng nói khi cố xác minh một trình đọc PDF phổ biến, họ tìm được "nhiều lỗi bảo mật trong một tuần bằng số lỗi thường được báo cáo trong một năm", và một lỗi logic ẩn hơn mười năm ở một ứng dụng khác. Cả hai không nêu tên phần mềm, không có số lỗi, nên Locaith không kiểm được.
- Máy móc do Claude tạo. Hãng nói Claude tự sinh mô hình lệnh của vi xử lý; bước qua từng lệnh thì khởi động được không gian người dùng Ubuntu trên nhân Linux, và quá trình sinh tìm ra hàng trăm lỗi trong tài liệu tham chiếu chính thức cùng một số nhỏ lỗi trong phần cứng. Đây là lời của hãng, chưa có nguồn độc lập.
Ý nghĩa với đội dùng thư viện mã nguồn mở
Cẩn thận với cách đọc "đã được chứng minh". Chứng minh trong kho chỉ nói về một điểm vào, về mã mà điểm vào đó chạm tới, trên bản biên dịch RISC-V tĩnh với musl, không phải bản x86-64 mà đa số máy chủ chạy. Danh sách đã chứng minh có openssl (bignum, pem, punycode…), zstd, simdjson, libpcap, mbedtls, nhưng chỉ cho từng bài fuzz cụ thể, nên một đội đang dùng các thư viện này không thể đọc đó là "thư viện đã được chứng minh an toàn". Điều khả dụng thực tế: chủ dự án mã nguồn mở có thể đăng ký miễn phí với Theorem; Theorem viết rằng phát hiện và bản vá do mô hình AI sinh và không hứa có người xem lại trước khi gửi, không đặt hạn công khai và không công bố các phát hiện. Với doanh nghiệp, tác dụng gián tiếp: các lỗi kiểu 20 MB hay 64 MB mà fuzzer ít chạm tới nhiều khả năng sẽ được tìm bằng cách này, nên kỳ vọng bản vá thượng nguồn nhiều hơn là tin vào chứng minh. Phần này là suy luận của Locaith, không phải khuyến nghị của Anthropic hay Theorem.
Đọc con số này thế nào
Các số 239 điểm vào, 123 thư viện, 180 triệu dòng Rocq, "hàng trăm lỗi", 40% ít token hơn, 17% ít token hơn, 99,95% khớp CPython đều là lời của Anthropic; chỉ phần 60 điểm vào / 25 dự án / 138 phát biểu / 20.164 phát biểu được Locaith đọc trực tiếp từ README và CHANGELOG của kho. Locaith không chạy bộ kiểm chứng minh, không kiểm các mô hình RISC-V/Linux (LPS), không kiểm đoạn Python/Verus và zlib. Phần so sánh 25% / 20% là phép chia của Locaith giữa hai con số không cùng mẫu số và không cùng bản dựng, chỉ để thấy phần người ngoài kiểm được nhỏ hơn thế nào.
Giới hạn của bài này
Locaith đọc ngày 25/10/2026 toàn văn bài của Anthropic (22/10; không đọc phụ lục), trang OSS Verify của Theorem, README, CHANGELOG và tài liệu nguồn gốc của kho, và bản ghi CVE gốc. Locaith không đọc bài của Theorem về lộ trình chứng minh toàn hệ sinh thái Nix, không đọc nhận xét của chuyên gia mà hãng dẫn, và chưa tìm thấy bản đánh giá độc lập nào của các chứng minh. Các nhận xét về chênh lệch giữa bài và kho là của Locaith.
Nguồn:
- Anthropic Frontier Red Team — LLMs are making formal software verification feasible at a much larger scale, 22/10/2026 — phương pháp, số liệu, hạn chế
- Theorem — OSS Verify — điều kiện đăng ký, nội dung nhận được, chính sách báo cáo
- Theorem — theorem-labs/oss-verify-proofs (README, CHANGELOG, docs/origin.md), bản 2026.10.0 ngày 22/10/2026 — số điểm vào/dự án/phát biểu, phạm vi phát biểu
- MITRE CVE — CVE-2026-56132 — bản ghi gốc của lỗi libexpat
Locaith đọc trực tiếp các nguồn trên ngày 25/10/2026. Ảnh bìa: tranh minh hoạ do Anthropic dùng cho bài của hãng, không phải ảnh về kết quả. Hai biểu đồ trong bài là của Anthropic, Locaith chỉ thu nhỏ. Ban Biên Tập Locaith biên soạn và phân tích ngày 25/10/2026.