Anthropic và Theorem đã sử dụng Claude để tạo các chứng minh hình thức trên 123 thư viện của OSS-Fuzz.

Mô hình Claude đã tạo ra các bằng chứng có thể kiểm chứng đối với các đặc tính an toàn trong 123 thư viện phần mềm. Dù đây là một bước tiến thực chất, điểm nghẽn kỹ thuật lại bị dịch chuyển: phần mềm đáp ứng chặt chẽ đặc tả hình thức, song bản thân đặc tả có thể bỏ sót các nguy cơ lỗi trong thực tế. Ngày 22/10/2026, Anthropic đã công bố kết quả hợp tác với Theorem: Claude đã tạo ra các chứng minh hình thức cho thấy 239 điểm kích hoạt kiểm thử ngẫu nhiên (fuzz test) thuộc 123 thư viện của OSS-Fuzz không gặp sự cố sập (crash) với bất kỳ dữ liệu đầu vào nào dưới 64 MB. Các chứng minh này được viết bằng Rocq, được hạt nhân (kernel) của trình hỗ trợ chứng minh kiểm tra, và hoạt động trực tiếp trên tệp nhị phân đã biên dịch cho kiến trúc RISC-V thay vì trên mã nguồn. Tổng khối lượng đạt khoảng 180 triệu dòng chứng minh; một chứng minh thông thường có độ dài hơn 600.000 dòng đối với một tệp nhị phân trung bình có 18.000 lệnh. Quy trình xuất phát từ bài kiểm thử fuzz test sẵn có của dự án. Bài kiểm tra này được chuyển đổi thành một phát biểu hình thức: theo mô hình tiến trình Linux và CPU RISC-V của Theorem, chương trình kết thúc mà không phát sinh lỗi bộ nhớ hoặc lỗi khẳng định (assertion failure) đối với mọi dữ liệu đầu vào trong giới hạn. Claude xây dựng bản chứng minh; Rocq kiểm tra tính tương thích giữa chứng minh và đặc tả kỹ thuật. Trong quá trình này, mô hình đã phát hiện và khắc phục các lỗi phát sinh — bao gồm việc phát hiện lại lỗ hổng CVE trong libexpat và những lỗi mà nhiều năm kiểm thử fuzzing chưa phát hiện được. Tuy nhiên, bản chứng minh chỉ xác nhận chính xác đặc tính đã được thiết lập: đơn luồng (single-thread), tệp nhị phân tĩnh, giới hạn bộ nhớ cố định, trên nền tảng mô phỏng RISC-V và Linux, với dữ liệu đầu vào tối đa 64 MB. Ngoài phạm vi này — chẳng hạn như môi trường đa luồng (multi-thread), thư viện glibc trên kiến trúc x86/ARM, hoặc các kịch bản chưa được nêu trong đặc tả — các bảo đảm trên không còn hiệu lực. Chính Anthropic cũng khẳng định rõ: "được kiểm chứng hình thức" không đồng nghĩa với việc "không có lỗi trong mọi trường hợp sử dụng thực tế". Thực tế này làm thay đổi cách tiếp cận đối với công tác kiểm chứng do AI hỗ trợ. Việc vượt qua các bài kiểm thử không còn là giới hạn cao nhất khi hệ thống có thể chứng minh việc không xảy ra lỗi sập trong một phạm vi xác định. Phần công việc phức tạp của con người sẽ chuyển dịch sang khâu khác: xây dựng đặc tả chính xác, xác định các yếu tố đưa vào hoặc loại trừ khỏi định lý, và đánh giá xem các giả định (mô hình hệ điều hành, kiến trúc phần cứng, giới hạn đầu vào) có bao quát được mức độ rủi ro chấp nhận được hay không. Công cụ chỉ kiểm chứng sản phẩm kỹ thuật; việc xác định các tiêu chuẩn cần đạt vẫn thuộc về trách nhiệm của đội ngũ kỹ sư. Đối với các đơn vị vận hành tác tử mã nguồn và quy trình an toàn, bài học thực tiễn rất rõ ràng: khi áp dụng chứng minh hình thức do AI tạo ra, danh mục kiểm tra không chỉ dừng lại ở câu hỏi "hạt nhân kiểm chứng đã chấp thuận hay chưa", mà phải mở rộng sang việc: những đặc tính nào đã được phát biểu, dựa trên các tiền đề nào, và những vấn đề nào doanh nghiệp vẫn cần xử lý ngoài phạm vi hình thức đó. Nếu thiếu các yếu tố này, bản chứng minh chỉ đơn thuần là sự xác nhận cho một bản đặc tả chưa hoàn chỉnh. Đọc toàn bộ bài viết bằng cách nhấp vào hình ảnh dưới đây: Tài liệu tham khảo Anthropic + Theorem, LLMs are making formal software verification feasible at a much larger scale (ngày 22/10/2026), 239 entry points, 123 thư viện OSS-Fuzz, ~180 triệu dòng Rocq, hợp ngữ RISC-V. Theorem oss-verify-proofs (tập hợp con công khai). Tác giả bộ sách "Kỹ thuật phần mềm có AI hỗ trợ" (hiện có trên Amazon). Tìm hiểu sâu chủ đề này một cách có hệ thống từ bối cảnh đến quản trị tác tử thông qua bộ sách bằng cách nhấp vào hình ảnh dưới đây: Mã giảm giá 30%: LEIA30 Đồng thời có sẵn trên Kindle Unlimited Từ khóa #EngenhariaDeSoftware #IA #VerificacaoFormal #Claude #Anthropic #Seguranca #OSSFuzz #Rocq #ProvasFormais #SoftwareEngineering #AI #FormalVerification #DevSecOps #Backend #RISC-V #Teorema #Especificacao