Anthropic cho biết Claude đã viết các chứng minh hình thức rằng 123 thư viện mã nguồn mở không thể bị sập

Trong một hợp tác với Theorem, Anthropic cho biết họ đã dùng Claude để chứng minh các thuộc tính bảo mật ở cấp độ assembly (RISC-V) trong hơn 100 thư viện mã nguồn mở đang được sử dụng thực tế. Công ty gọi đây là lần đầu AI được dùng trên quy mô lớn để xác minh hình thức phần mềm sản xuất ở cấp độ này.

Theo Anthropic:

• Đã chứng minh điều gì: với 239 điểm đầu vào kiểm thử fuzz trên 123 thư viện OSS-Fuzz, chương trình luôn kết thúc bình thường, không có lỗi an toàn bộ nhớ hay khẳng định thất bại, với mọi đầu vào dưới 64 MB. Điều này đúng theo các giả định: tệp nhị phân tĩnh, đơn luồng, ngân sách bộ nhớ cố định, chạy trên CPU RISC-V dùng Linux. Các chứng minh có tổng cộng khoảng 180 triệu dòng Rocq, được bộ kiểm tra chứng minh Rocq xác minh.
• Cách thực hiện: kiểm thử fuzz hiện có của mỗi thư viện được chuyển thành một đặc tả (“kiểm thử này không bao giờ làm chương trình bị sập”), rồi Claude viết chứng minh và vá các lỗi phát hiện được trong quá trình này. Anthropic cho biết cách làm này tìm ra hàng trăm lỗi, kể cả những lỗi mà trình fuzz khó có thể chạm tới, chẳng hạn lỗi ghi vượt giới hạn cần một đầu vào hiếm dài 20 MB, và phát hiện lại CVE-2026-56132 trong libexpat.
• Các thử nghiệm khác: Claude chứng minh rằng phần triển khai zlib của Linux khớp với đặc tả RFC 1950 ở cấp độ tệp nhị phân x86, đồng thời xây dựng một trình thông dịch Python bằng Rust có hành vi khớp với CPython trong 99,95% trên 1,7 triệu chương trình ngẫu nhiên. Anthropic cũng cho biết các nỗ lực xác minh hình thức trên một trình đọc PDF được sử dụng rộng rãi đã phát hiện số 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.
• Chi phí: các chứng minh có thể cần hàng trăm triệu token. Trên 36 tác vụ xác minh nhỏ, Anthropic cho biết Opus 5.5 chứng minh được một nửa số tác vụ với lượng token ít hơn khoảng 40% so với Opus 5, và các tác tử chia sẻ chứng minh cần ít hơn 17% token.

Anthropic đang công bố một phần các chứng minh cùng với ngữ nghĩa RISC-V và Linux. Theorem đề nghị chạy cùng quy trình này cho các dự án mã nguồn mở khác và đang công bố một kỹ năng Claude để bạn xác minh mã của mình. Anthropic lưu ý rằng điều này không chứng minh các thư viện không có lỗi: những lỗi còn lại sẽ nằm trong các thành phần được tin cậy hoặc ngoài phạm vi của các chứng minh.