Đội red team tiên phong (Frontier Red Team) của Anthropic ngày 22/10 công bố một nghiên cứu: dù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ở, khẳng định rằng với đầu vào nhỏ hơn 64 MB, các chương trình này sẽ không bị crash. Chứng minh được thực hiện trực tiếp trên tệp thực thi RISC-V đã biên dịch, với đối tác là Theorem, công ty chuyên về công cụ xác minh hình thức. Anthropic cho biết đây là lần đầu tiên AI thực hiện xác minh hình thức ở quy mô lớn ngay tại tầng assembly của phần mềm sản xuất.
Toàn bộ các thư viện này đến từ dự án OSS-Fuzz của Google, tức nhóm thành phần nền tảng được chạy fuzzing liên tục trên nền tảng này, trong đó có nén dữ liệu, giải mã ảnh và phân tích cú pháp HTTP. Toàn bộ công trình mất vài tuần.
Biến bài kiểm thử fuzzing thành định lý
Cách làm gồm ba bước. Bước một, nhóm viết lại bộ kiểm thử fuzz sẵn có của mỗi thư viện thành một đặc tả hình thức, với ý nghĩa là “đoạn mã kiểm thử này không crash với mọi đầu vào”. Đặc tả được xây trên mô hình ngữ nghĩa tập lệnh RISC-V và ngữ nghĩa tiến trình Linux do Theorem cung cấp.
Bước hai giao cho Claude viết chứng minh, sau đó trình kiểm tra chứng minh Rocq đối chiếu từng bước.
“Claude writes the proof; the Rocq kernel checks it against the specification.” (Claude viết chứng minh, còn nhân Rocq đem nó đối chiếu với đặc tả để kiểm tra.)
Bước ba xử lý trường hợp chứng minh không đi tiếp được. Chứng minh bế tắc thường có nghĩa là trong mã thực sự có lỗi; khi đó Claude tự sửa mã, đặc tả được sinh lại rồi tiếp tục chứng minh. Nhóm thừa nhận bước này dễ nảy sinh hiện tượng “reward hacking”: mô hình có thể sửa chương trình bừa bãi chỉ để chứng minh qua được. Vì vậy họ thêm hình phạt cho các bản vá, yêu cầu chứng minh phạm vi đầu vào mà bản vá ảnh hưởng, đồng thời ghi lại từng bản vá và để con người kiểm toán.
Một chứng minh điển hình dài khoảng 600.000 dòng. Phần cuối cùng cần tin cậy chỉ còn mô hình ngữ nghĩa của RISC-V và Linux, phát biểu của chính định lý, và trình kiểm tra Rocq.
Những lỗi được tìm ra trong quá trình chứng minh
Trong lúc chứng minh, nhóm đã phát hiện và sửa hàng trăm lỗi, trong đó có những lỗi rất khó tìm ra bằng fuzzing. Bài viết nêu vài ví dụ: một bộ giải nén bị tràn số âm (underflow) ở bộ đếm, chỉ kích hoạt với một số đầu vào đặc biệt khoảng 20 MB; một bộ giải mã ảnh đọc ngoài biên, cần đầu vào 64 MB cùng hơn 2 GB bộ nhớ mới xuất hiện; còn một lỗi đọc ngoài biên khác đòi hỏi hai handle thao tác trên cùng một tệp theo một thứ tự nhất định. Lỗ hổng CVE-2026-56132 của libexpat cũng được phát hiện lại một lần nữa.
Chứng minh cho cpp-httplib có thêm một rào cản: việc đệ quy khi hủy std::set có thể gây tràn ngăn xếp. Để loại trừ khả năng này, nhóm đã chứng minh ở cấp mã máy rằng thuật toán cân bằng cây đỏ-đen của libc++ giữ độ sâu cây ở mức logarit.
Cùng bài nghiên cứu còn kèm theo vài thí nghiệm bên lề. Claude dùng Rust viết một tập con của Python, rồi dùng Verus chứng minh nó tuân theo ngữ nghĩa CPython; trên 1,7 triệu chương trình ngẫu nhiên, tỷ lệ hành vi trùng với CPython đạt 99,95%. Claude cũng tự sinh ra một bộ ngữ nghĩa lệnh x86, chạy từng bước đơn lẻ có thể khởi động không gian người dùng Ubuntu, và nhân tiện tìm ra hàng trăm chỗ sai trong tài liệu tham chiếu chính thức.
Đặt cạnh seL4 để so sánh
Xác minh hình thức không phải điều mới mẻ trong công nghiệp; khó khăn từ trước đến nay nằm ở nhân lực. Giới chuyên môn thường lấy vi nhân seL4 làm ví dụ: khoảng một vạn dòng mã C, công sức chứng minh thuở ấy thường được nhắc tới là cỡ hai mươi người-năm. Trình biên dịch CompCert cũng đi theo hướng tương tự, được một nhóm nhỏ mài giũa nhiều năm. Điểm chung của các dự án này là đối tượng ít, chu kỳ dài, chuyên gia dày đặc.
Quy mô lần này của Anthropic là 123 thư viện trong vài tuần; đối chiếu sơ bộ, cấu trúc chi phí trên mỗi đơn vị công việc đã mang một hình hài khác, con người lùi từ việc viết chứng minh sang việc định đặc tả và duyệt bản vá. Cái giá chuyển sang token: bài viết cho biết một chứng minh hoàn chỉnh có thể tiêu tốn hàng trăm triệu token. Trên 36 tác vụ nhỏ, mỗi tác vụ cho một agent ba lần thử, mỗi lần ngân sách 5 triệu token; khi cho phép các agent tái sử dụng chứng minh của nhau, lượng token cần thiết giảm thêm 17%.
Mức độ đảm bảo của hai bên cũng không cùng một tầng. seL4 chứng minh tính đúng đắn về chức năng, còn lần này chỉ chứng minh “không crash”, phạm vi hẹp hơn nhiều.
Những khoảng trống ngoài phạm vi chứng minh
Các hạn chế mà Anthropic tự liệt kê khá cụ thể. Chứng minh dựa trên tệp nhị phân RISC-V đơn luồng, liên kết tĩnh và dùng musl libc, trong khi đa số người dùng thực tế chạy phiên bản x86 hoặc ARM liên kết động với glibc. Bản thân AddressSanitizer không bắt được mọi lỗi an toàn bộ nhớ, một số điểm vào chưa được bao phủ, và hỏng bộ nhớ do bên gọi dùng sai thư viện cũng nằm ngoài phạm vi chứng minh.
“Formally verified” does not mean “bug-free.” (“Được xác minh hình thức” không có nghĩa là “không có bug”.)
Độ lệch giữa đặc tả và máy thật là chỗ dễ xảy ra sự cố nhất của hướng đi này. Bản thân Rocq và các bộ mô hình ngữ nghĩa cũng cần được gia cố, bài viết nói việc này “không hề nhỏ”. Nhận định của nhóm là xác minh hình thức sẽ trở thành một khâu thường lệ trong phát triển phần mềm an toàn; còn khi nào các chứng minh này phủ được những môi trường triển khai phổ biến như x86 và glibc thì bài viết không nêu mốc thời gian.
Nguồn tham khảo: bài nghiên cứu của Frontier Red Team thuộc Anthropic, CocoLoop; trang nghiên cứu của Anthropic được dùng để đối chiếu số thư viện, số điểm vào, số dòng chứng minh và cách tính khi so sánh token.