Anthropic Mengatakan Claude Membuktikan Sifat Keamanan pada 123 Pustaka

Pada 22 Oktober 2026, Anthropic menerbitkan penelitian yang melaporkan bahwa Claude menghasilkan bukti formal yang diperiksa mesin tentang sifat keamanan pada tingkat kode rakitan RISC-V untuk 239 titik masuk uji fuzz di 123 pustaka sumber terbuka, dalam kolaborasi dengan Theorem.

Menurut Anthropic, Claude memperbaiki bug yang ditemukannya, lalu membuktikan bahwa program akan selalu berhenti secara normal tanpa memicu kesalahan keamanan memori atau gagal memenuhi pernyataan, untuk setiap masukan berukuran di bawah 64 MB dan setiap respons sistem operasi Linux serta tata letak memori yang dimodelkan. Bukti tersebut mengasumsikan program berjalan sebagai biner statis berutas tunggal dengan anggaran memori tetap pada CPU RISC-V yang menggunakan Linux. Anthropic mengatakan bukti-bukti itu terdiri atas sekitar 180 juta baris Rocq, dengan bukti tipikal sepanjang sekitar 600.000 baris untuk mencakup biner yang panjang mediannya 18.000 instruksi RISC-V. Perusahaan itu mengatakan bahwa, sejauh pengetahuannya, ini merupakan upaya skala besar pertama yang menggunakan AI untuk menerapkan verifikasi formal pada perangkat lunak produksi di tingkat kode rakitan.

Sebagian bukti, beserta semantik RISC-V dan sistem operasi yang mendasarinya, sedang dipublikasikan di GitHub. Anthropic mengatakan pihaknya juga merilis komponen tepercaya yang dibuat untuk proyek tersebut dan belum tersedia untuk umum, bukti lengkap untuk uji fuzz yang tidak memerlukan perbaikan, serta spesifikasi untuk uji fuzz yang tidak dapat dibuktikannya, sementara bukti yang dapat mengungkap bug yang belum diperbaiki tidak dipublikasikan.

Mengubah Uji Fuzz Menjadi Bukti Formal

Pendekatan ini mengubah uji fuzz yang sudah ada dan dapat dikompilasi di setiap pustaka menjadi spesifikasi formal yang memuat satu aturan: uji tersebut tidak pernah mengalami crash untuk masukan apa pun yang berukuran di bawah 64 MB. Spesifikasi itu didefinisikan berdasarkan instruksi RISC-V yang telah dikompilasi, dengan menggunakan semantik formal Theorem untuk set instruksi RISC-V dan proses Linux. Pemeriksa bukti Rocq kemudian memverifikasi setiap bukti yang telah selesai berdasarkan spesifikasi tersebut. Anthropic mengatakan bahwa dengan demikian, hanya ada tiga komponen yang perlu dipercaya oleh pengembang: model formal RISC-V dan proses Linux, pernyataan teorema yang tepat, serta pemeriksa Rocq itu sendiri.

Anthropic mengatakan pihaknya menerapkan proses ini pada ratusan proyek dalam inisiatif OSS-Fuzz milik Google, yang menyediakan pengujian fuzz berkelanjutan untuk proyek sumber terbuka yang memenuhi syarat dan secara otomatis menyisipkan instrumentasi ke program C dan C++ menggunakan AddressSanitizer, alat yang membuat program mengalami crash setiap kali terjadi akses memori yang tidak semestinya. Lampiran bertanggal 22 Oktober 2026 menguraikan teorema lengkap yang dibuktikan: untuk semua masukan berukuran di bawah 64 MiB dan semua tata letak memori, baik biner yang diberi instrumentasi ASan maupun biner biasa tidak mengalami kesalahan akses, berhenti paksa, atau menunjukkan perilaku yang tidak dimodelkan; keduanya juga menghasilkan jejak baca dan tulis, perilaku saat berhenti, serta keadaan akhir sistem berkas yang identik.

Lampiran tersebut menyatakan bahwa Claude menulis sekitar satu miliar baris Rocq selama upaya ini, dan sekitar 180 juta baris di antaranya lolos pemeriksaan bukti. Titik masuk parser cJSON yang terdiri atas 391 baris mendapat bukti sepanjang 630.000 baris, sedangkan fftw3, dengan 51.000 baris kode yang ditautkan ke dalamnya, mendapat bukti sepanjang 480.000 baris. Karena Claude diizinkan memperbaiki kode sebelum menyelesaikan pembuktian, Anthropic mengatakan pihaknya mengurangi nilai untuk perbaikan, memberikan kredit tambahan untuk membuktikan masukan mana saja yang berubah akibat suatu perbaikan, serta mencatat dan mengaudit perbaikan guna mencegah manipulasi sistem imbalan.

Bug yang Ditemukan Selama Upaya Pembuktian

Anthropic melaporkan bahwa upaya pembuktian mengungkap ratusan bug, banyak di antaranya kemungkinan besar tidak akan ditemukan oleh alat fuzzing. Saat membuktikan titik masuk salah satu pustaka, Claude menemukan underflow pada penghitung di sebuah dekompresor yang menyebabkan penulisan di luar batas, tetapi hanya pada masukan berukuran sekitar 20 MB dengan satu tata letak tertentu yang jarang terjadi. Temuan lainnya mencakup pembacaan di luar batas pada dekoder gambar yang memerlukan masukan 64 MB dan memori lebih dari 2 GB, pembacaan di luar batas yang memerlukan urutan panggilan tertentu melalui dua handel ke berkas yang sama, serta penemuan kembali CVE-2026-56132 di libexpat, yang memerlukan masukan bertingkat sangat dalam.

Claude juga menemukan bug logika yang tidak pernah menyebabkan crash, termasuk pembatasan terhadap berkas yang dapat dimuat oleh suatu aplikasi, yang tidak selalu diberlakukan. Anthropic mengatakan upaya verifikasi pada beberapa aplikasi penting yang banyak digunakan mengungkap bug logika yang sebelumnya tidak diketahui dan telah tersembunyi selama lebih dari satu dekade. Perusahaan itu juga mengatakan bahwa dalam upaya memverifikasi pembaca PDF yang banyak digunakan, pihaknya menemukan jumlah bug keamanan dalam satu minggu yang biasanya dilaporkan selama setahun.

Eksperimen Tambahan dan Temuan Efisiensi

Selain OSS-Fuzz, Anthropic meminta Claude menulis spesifikasi formal RFC 1950, dokumen teknis yang mendefinisikan format kompresi zlib, lalu membuktikan bahwa implementasi zlib di kernel Linux menerapkannya dengan benar. Claude membuktikan langsung biner yang dikompilasi untuk x86 dengan menggunakan semantik formal set instruksi x86 yang dihasilkan Claude. Anthropic mengatakan pihaknya mengulangi proses tersebut pada setengah lusin pustaka lain yang banyak digunakan dan menemukan bug kecil pada kasus-kasus khusus yang tidak dapat dieksploitasi, yang sedang dilaporkan kepada pengelola proyek terkait. Perusahaan itu juga melaporkan bahwa pembuatan semantik x86 mengidentifikasi ratusan kesalahan dalam dokumentasi referensi resmi dan sejumlah lebih kecil bug pada perangkat keras itu sendiri, serta bahwa penelusuran langkah demi langkah melalui semantik tersebut dapat mem-boot lingkungan pengguna Ubuntu pada kernel Linux.

Dalam eksperimen lain, Claude membangun interpreter untuk sebagian besar bahasa Python menggunakan Rust dan membuktikan, dengan alat verifikasi Verus, bahwa interpreter tersebut mematuhi semantik CPython yang diuraikan dalam sebuah makalah akademis. Lampiran teknis menyatakan bahwa seluruh 17 tingkat interpreter telah dibuktikan, dengan teorema yang menyatakan, “Setiap kali interpreter mengembalikan hasil, hasil tersebut adalah hasil yang ditentukan oleh semantik formal.” Anthropic mengatakan bahwa pengujian empiris terhadap 1,7 juta program Python yang dihasilkan secara acak menemukan perilaku yang identik dengan CPython dalam 99,95% pengujian; dari tujuh bug yang sengaja disisipkan, lima tidak terdeteksi oleh pengujian acak, sedangkan ketujuhnya menggagalkan pembuktian.

Untuk mengukur efisiensi, Anthropic membuat 36 tugas verifikasi kecil dengan menyederhanakan titik masuk OSS-Fuzz yang sebenarnya, sehingga menghasilkan program sepanjang 283–2.491 instruksi dengan masukan yang dibatasi hingga 64 byte dan AddressSanitizer digantikan oleh runtime “mini-ASan” yang terdiri atas sekitar 100 instruksi. Anthropic melaporkan bahwa Opus 5.5 membuktikan separuh tugas tersebut dengan sekitar 40% lebih sedikit token dibandingkan Opus 5. Anthropic juga melaporkan bahwa agen yang diizinkan menyalin pembuktian satu sama lain di ruang kerja bersama membutuhkan 17% lebih sedikit token daripada agen yang bekerja sendiri; beberapa agen berhasil setelah sebelumnya gagal saat bekerja sendiri, sementara agen yang bekerja sendiri tidak berhasil menyelesaikan dua pembuktian. Perusahaan itu mengatakan bahwa efek penggunaan ulang yang sama juga terlihat dalam skala besar selama upaya OSS-Fuzz, ketika tim agen menyalin pembuktian yang telah selesai dan menyesuaikannya karena sebagian besar setiap pembuktian mencakup kode runtime C dan inisialisasi AddressSanitizer yang digunakan bersama.

Keterbatasan yang Diungkapkan dan Program OSS Verify

Anthropic menyatakan bahwa pembuktian tersebut tidak berarti pustaka-pustaka itu bebas dari bug: bug yang masih ada mungkin berada di dalam komponen tepercaya atau di luar cakupan pembuktian. Pembuktian tersebut mencakup biner RISC-V statis berutas tunggal yang ditautkan dengan musl libc, sementara sebagian besar pengguna menjalankan pustaka-pustaka ini pada x86 atau ARM dan menautkannya secara dinamis dengan glibc; selain itu, AddressSanitizer tidak mendeteksi semua bug keamanan memori. Perusahaan itu mengatakan bahwa pihaknya memperkirakan keterbatasan ini akan dapat diatasi seiring dengan peningkatan kemampuan model.

Theorem menawarkan alur kerja yang sama secara gratis kepada proyek sumber terbuka yang memenuhi syarat melalui program OSS Verify. Pendaftaran dilakukan dengan mengajukan pull request yang menambahkan berkas project.yaml, Dockerfile, dan build.sh ke repositori program tersebut. Theorem mengatakan bahwa proyek ditinjau dengan kriteria yang serupa dengan OSS-Fuzz, dengan memprioritaskan infrastruktur penting yang digunakan secara luas. Menurut Theorem, para pemelihara proyek menerima pembuktian Rocq, yang diperiksa oleh kernel Rocq, bahwa setiap target fuzz tidak mengalami crash pada masukan apa pun hingga 64 MiB; bug yang ditemukan selama upaya pembuktian akan disampaikan secara pribadi kepada para pemelihara melalui email tanpa tenggat waktu pengungkapan, dan pembuktian dapat memerlukan waktu beberapa hari. Peta jalan Theorem menargetkan verifikasi seluruh ekosistem Nix, termasuk infrastruktur penting seperti glibc, OpenSSL, dan cURL.